CWI Scanprofile/PDF/300 Centrum voor Wiskunde en lnformatica Centr~ for Mathematics and Computer Science M. Bezem Semantics and consistency of rule-based expert systems ~ Computer Science/Department of Software Technology Report CS-R8824 July The Centre for Mathematics and Computer Science is a research institute of the Stichting Mathematisch Centrum, which was founded on February 11, 1946, as a nonprofit institution aim- ing at the promotion of mathematics. computer science, and their applications. It is sponsored by the Dutch Government through the Netherlands Organization for the Advancement of Pure Research (Z.W.0.). Copyright ~ Stichting Mathematisch Centrum, Amsterdam ,. &q !.( l ~I"°:} I< 14 1bl3 \~ 4 { Semantics and Consistency of Rule-based Expert Systems Marc Bezem Centre for Mathematics and Computer Science P.O. Box 4079, 1009 AB Amsterdam, The Netherlands Consistency of a knowledge-based system has become a topic of growing concern. Every notion of con- sistency presupposes a notion of semantics. We present a theoretical framework in which both the seman- tics and the consistency of a knowledge base can be studied. This framework is based on first order flat many-sorted predicate logic and is sufficiently rich to capture an interesting class of rule-based expert sys- tems and deductive databases. We analyse the feasibility of the consistency test and prove that this test is feasible for knowledge bases in Horn format without quantification. This report is a revised and extended version of report CS-R8736. The extension concerns the use of expressions in rules. 1980 Mathematics Subject Classification: 68T30, 68T15. 1987 CR Categories: 1.2.3, 1.2.4, F.4.1. Key Words & Phrases: knowledge-based systems, rule-based expert systems, knowledge representation, consistency. Note: The material for this article has been taken from the PRISMA documents P176 and P297. The research is part of the PRISMA project (PaRallel Inference and Storage MAchine), a joint effort with Philips Research Eindhoven, partially supported by the Dutch "Stimulerings-projectteam lnformatica-onderzoek" (SPIN). INTRODUCTION The plan of this paper (a revised and extended version of [BJ) is as follows. First the reader is intro- duced to the knowledge representation used in rule-based expert systems. We shall indicate some semantical problems in relation to this knowledge representation. Then we explain in an informal way how many-sorted predicate logic comes in. In the next section we describe syntax and semantics of many-sorted predicate logic. We assume some knowledge of first order logic. Thereafter we shall be able to characterize rule-based expert systems as first order theories. The Tarski semantics solves the semantical problems mentioned above. Furthermore we shall derive several results on decidability and consistency of rule-based expert systems. Unfortunately, some natural equality and ordering axioms are not in Hom format (see [Re] for a discussion on the domain closure axiom). Hence test- ing consistency with a standard theorem prover would be very inefficient. In the fourth section we describe a technical device, a certain kind of null value, which allows feasible consistency testing in the presence of equality and ordering axioms, which are not in Hom format. The underlying idea is partiality of functions, thus avoiding the search for consistent function values in a (possibly gigantic) product space. This kind of null value, being quite different from null values as described in [IL], appears to be new. In the last section we show how to extend our results to knowledge bases with arithmetical (and other) expressions in the conditions of the rules. We shall focus our attention on rule-based expert systems, but the techniques can also be applied to deductive databases with func- tional dependencies. Report CS-R8824 Centre for Mathematics and Computer Science P.O. Box 4079, 1009 AB Amsterdam, The Netherlands 2 1. RULE-BASED EXPERT SYSTEMS l. L In rule-based expert systems shells such as EMYCIN [BS] or DELFI2 [L], knowledge about some specific domain can be expressed in facts and in rules of the form IF antecedent THEN consequent. Facts are so-called object-attribute-value triples, or triples for short. The antecedent of a rule is a conjunction of disjunctions of conditions, and conditions are definite statements, such as same, notsame and less than, about . In most cases so-called certainty factors are associated with the facts and the rules. Certainty factors range from LOO (definitely true) to - LOO (definitely false). ~e certainty factor of a fact expresses a measure of certainty about that fact, whereas the certainty factor of a rule scales the measure of certainty about the consequent with respect to the measure of certainty about the antecedent. In DELFI2 an object tree (called context tree in MYCIN) is used to state properties of and relations between different objects, which cannot be expressed by the rules. The nodes of this tree are objects, labeled by their attributes and respective domains of values. The path from a node to the root of this tree constitutes the context of that node. In other words: the objects occurring in the subtree of a node are sub-objects of the object belonging to that node. Furthermore it is stated in the object tree whether an attribute is singlevalued or mul- tivalued. The interpretation of the knowledge in rule-based expert systems is more operational than declara- tive: same is true if and only if occurs as fact (with certainty factor > 0.2), conclude has the effect that is added as fact (with appropriate certainty factor), and if the antecedent of a rule evaluates to true, then that rule may be fired, i.e. all conclusions occurring in the consequent are executed. We remark that same and conclude have the same declarative meaning as the fact , i.e. attribute a of object o has value v. L2. Consider the following real-life example extracted from HEPAR, an expert system for the diag- nosis of liver and biliary disease, built with DELFI2. IF same THEN conclude (LOO) IF same (-LOO) IF same OR same THEN conclude (1.00) and (LOO). The inference engine reasons backwards, using a simple loop check to prevent infinite looping. Depending on the presence of the fact (1.00), the inference engine did or did not hit upon the contradiction (1.00 and -1.00). In both cases the contradiction was completely ignored. These observations show a defect of the knowledge representation used in rule-based expert sys- tems, namely the lack of a dear semantics. 1.4. Basically our approach amounts to interpreting (o,a,v> by a(o,v) in the multivalued, and by a( o) = v in the singlevalued case. Here o and v are constants for elements of a domain 0 of objects and a domain V of values. In the multivalued case a denotes a relation, i.e. a subset of 0 X V, and in the singlevalued case a function from 0 to V. If o is a sub-object of o', then o' is added as argument of a. 1.5. The following examples show how to extend our interpretation of triples to atoms. conclude becomes complaint (patient,abdominal _pain) less _than becomes temperature (patient) < 36.8 same becomes character (patient,pain) = continuous Note that the fact that pain is a sub-object of patient is expressed by adding patient as an argument of the function character. Another example, based on the rules of 1.2, is to be found in 4.6. We feel that the existing formalisms for handling uncertainty are unsatisfactory. As we do not have a good alternative we leave the subject aside. 1.6. Under the interpretation described above, a rule-based expert system becomes a theory in first order many-sorted predicate logic, in short: a many-sorted theory. To keep this paper self-contained we give a short, introductory description of the syntax and semantics of many-sorted predicate logic in the next section. In Section 3 we shall characterize expert systems as many-sorted theories of a cer- tain type. This approach has the following advantages: - The declarative semantics of the expert system becomes perfectly clear, being the Tarski semantics of the associated many-sorted theory. - Logical concepts such as consequence, consistency and decidability get a clear meaning in relation to the expert system. - Theorem proving techniques for testing consistency, such as resolution, become available for the expert system. 4 The choice for many-sorted instead of one-sorted logic is motivated as follows: - It is natural to make a distinction between numerical data (ordered by <)and symbolic data (usu- ally unordered). - Subdividing a set of constants into sorts and typing the predicate and function symbols considerably reduces the number of well-formed formulas, which is important for debugging large knowledge bases. - In the presence of variables the many-sorted approach imposes restrictions on unification, which considerably reduces the resolution search space (see for example [W]). We shall not make use of this advantage in the present paper. 2. MANY-SoRTED PREDICATE LoGIC 2.1. The syntax of many-sorted predicate logic extends the syntax of ordinary, one-sorted, predicate logic by having a set of sorts ~. instead of just one sort. Moreover we have variables xr and constants er for all sorts GE~. Furthermore we have function symbols fl' x ... Xam-->O), where the notion of type G1 X · · · XGm~Go replaces the notion of arity from the one-sorted case. We also have proposi- a X ••· Xa f f tion symbols p; and predicate symbols P;' m (m>O) 0 type G1 x ... XGm· Terms are ormed from variables and constants by function application (respecting the sorts). Atoms are either proposi- tion symbols or the application of a predicate symbol to terms of appropriate sorts. With the help of propositional connectives and quantifiers, atoms are combined into formulas. The sets ~. CONS, FUNC, PROP and PRED of, respectively, sorts, constants, function symbols, proposition symbols and predicate symbols, form together the similarity type of a specific many-sorted predicate calculus. For practical reasons we assume that the similarity type is finite. 2.2. A many-sorted structure 01L consists of: (a) A non-empty set Aa for each GE~, called the domain of sort G. (b) For each constant er an element Cj E Aa. (c) For each function symbol fl'x · · · xam-->ao a mapping]; : Aa, X · · · XAam ~Aa.· ( d) For each proposition symbol p; a truth value p;. _ (e) For each predicate symbol Pf'x ··· xam a mapping P; : Aa, X · · · XAam ~{TRUE,FALSE}. 2.3. An assignment in 01Lis a mapping a assigning to each variable xr an element a(x7) of Aa. 2.4. The interpretation in 01L of a term t under an assignment a, denoted by ./'ff(t) or t for short, is inductively defined as follows: (a) xr = a(x7) (b) er = Cj () j'OX···Xa-->a0 ( ) f-(- -) c J ;' m t,,. .. ,tm = ; ti. ... ,Im The truth value in 01L of an atom Pf'x · · · xam(t 1,. • .,tm) under an assignment a is given by P;(ti. ... , tm). 2.5. The truth value in 01L of a formula F under an assignment a, denoted by ~(F), is inductively defined as follows: (a) If Fis an atom, then ~(F) is given by 2.4. (b) ~ respects the truth tables of the propositional connectives. (c) ~<:rfxr F) = TRUE if and only if for all assignments a', which differ at most on xr from a, we have Cl,f/}(F) = TRUE. (d) ~(3xr F) = TRUE if and only if there exists an assignment a', which differs at most on xr from a, such that Cl,f}(F) = TRUE. 5 2.6. A formula Fis true in~ denoted by l='!JR,F, if ci.ff(F) = TRUE for all assignments a. 2.7. A sentence (or closed formula) is a formula without free variables (i.e. variables which are not bound by a quantifier). It will be clear that for sentences S the truth value ci.ff(S) does not depend on the assignment a. As a consequence we have either l='!Jf(,S or l='!JR,-,S, for every sentence S. Let SENT denote the set of sentences. · 2.8. Let f C SENT. ~is called a model for f, denoted by l='!JR,f, if l='!JR,S for all S ef. 2.9. S E SENT is called a (semantical) consequence of (or implied by) r c SENT if for all many- sorted structures~ we have: if l='!JR,f, then l='!JR,S. This will be denoted by f 1= S (or 1= S if r is empty). Furthermore we define the theory off as the set Th(f) = {S E SENT I f 1= S}. 2.10. f c SENT is called consistent if f has a model. Th(f) is called decidable if there exists a mechanical decision procedure to decide whether a given sentence S is a semantical consequence of r or not. 2.11. Two many-sorted structures are called elementarily equivalent if exactly the same sentences are true in both structures. 2.12. REMARKS. 2.12.1. We refrain from giving an axiomatization of many-sorted predicate logic since our main con- cern will be model theory. Most textbooks on mathematical logic provide a complete axiomatization of ordinary (one-sorted) predicate logic. It suffices to generalize the quantifier rules in order to obtain an axiomatization of flat many-sorted predicate logic. 2.12.2. Of course, one-sorted predicate logic is a special case of many-sorted predicate logic. As a consequence, the latter is as undecidable as the former. More precisely: 1= S is undecidable, provided that the similarity type is rich enough ( CHuRcH, TuruNG, 1936, see also [M, 16.58)). 2.12.3. Conversely, many-sorted predicate logic can be embedded in one-sorted predicate logic by adding unary predicate symbols S" (x ), expressing that x is of sort o, and replacing inductively in for- mulas VxY F (resp. 3x7 F) by Vx(S"(x)~F) (resp. 3x(S"(x)AF)). Let A' be the one-sorted sentence obtained from A E SENT in this way. It can be proved (see [M]) that I= A if and only if r I= A', where r = {3xS"(x)loe~} expresses the fact that the domains are non-empty. This embedding allows us to generalize immediately many results on one-sorted predicate calculus to the many-sorted case (e.g. the compactness theorem). We shall not make use of this possibility in the present paper. 3. RULE-BASED ExPERT SYSTEMS AS MANY-SORTED THEORIES 3.0. We propose the following terminology for certain kinds of many-sorted theories: - Indexed propositional expert systems. - Universally quantified expert systems. 3.1. An indexed propositional expert system is a many-sorted theory axiomatized by: (a) Explicit axioms (the rule base and the fact base), which are boolean combinations of atoms of the f P11,X ••• Xu.,( ') f th f 1<11,x ••• X11.,)-->l10( ') - II ( < II > II) orm c,. .. ,c or o e orm c, ... ,c - 110 c resp. 110 c , 110C , with constants c, .. .,c1,c11 of appropriate sorts. Such atoms (here and below called constant-atoms, or c-atoms for short) may be viewed as indexed propositions, which explains the name. Note that we conform to the convention to write =, < and > as infix predicates. 6 (b) Implicit axioms for equality of each sort and ordering of each sort for which an ordering is appropriate. The axioms for =0 , equality of sort 11, are (loosely omitting sort super- and sub- scripts): 'r:/x(x =x), Vxi,x 2(x 1 =x2~X2 =x 1), 'r:/xi,x2,x 3((x1 =x2/\x2 =x3)~x 1 =x 3 ), 'r:/xi,x2((x 1 =x2/\F(x1))~F(x2)) for formulas F, -,ci=cj for O~i=/=j~n, 'r:/x(x =c0 v · · · Vx =en), the domain closure axiom. These axioms express that = is a congruence relation on a finite domain, where every element has exactly one name. Let EQ denote the set of equality axioms for all sorts 11, then we have by definition that either EQ 1= c;=cj or EQ I= -,c;=cj for all i,j. The axioms for< and> are: 'r:/xi,x2,X3((x1 x1), a subset A of { c; . Let 0 denote the set of ordering axioms. We require that A is such that either 0 1= ci···•tn is an assignment of a unique element of the appropriate domain A 0 to each tj (1-s;;;jos;;;;n). It will be clear that a truth valuation of P1> .. .,Pm and a valuation of t1> .. .,tn suffice for an interpretation of f. Each model off yields a truth valuation of P1,. . .,Pm and a valuation of IJ> .. .,tn. Conversely, each truth valuation of PJ> .. .,Pm and valuation of t 1,. • .,tn for which every explicit axiom of r is true, can be extended in an arbitrary way to a many-sorted structure~ 1= f. Thus we have the following THEOREM. Let conditions be as above. Then we have: r is consistent if and only if there exists a truth valuation of P 1>··· ,Pm and a valuation oft 1,. . ., tn for which every explicit axiom of r is true. 4.2. Theorem 4.1 suggests a simple algorithm for testing the consistency of an indexed propositional expert system f: generate all valuations and truth valuations and test each time whether the explicit 8 axioms of f are satisfied or not. This clearly leads to combinatorial explosions. A second step towards a feasible consistency test is imposing language restrictions on our expert systems. A common language restriction is Horn format. A clause is a finite disjunction of atoms and nega- tions of atoms (so called positive and negative literals). A conjunctive normal form is a finite conjunc- tion of clauses. A Horn clause is a clause containing at most one positive literal. A unit clause is a clause consisting of one positive literal. The connection between Horn clauses and production rules is easily seen by the equivalence of (A 1 /\ • • • /\Ak) ~ B and A 1 v · · · v A;; v B+, where the super- scripts + and - denote whether a literal occurs positively or negatively. However, the implicit axioms 'Vx(x =coV · · · Vx =en) and 'Vxi,x2(x1 c;for a/l I:o;;;;;;i:o;;;;;;n. (4) The orderings < and> do not occur in the positive literals occurring in the explicit axioms off. Then the consistency off can be tested in polynomial time. PRooF. List the explicit axioms of r as follows (the super- and subscripted capitals denote c-atoms): At Aj CI,"1 V · · · VCI,"n, vDt Ci,1 V • · • VCi,n, V Di BI,"1 V • • • VBI,"m, B;:1 v · · · v B;:m, 9 Now apply the following algorithm, which is in fact a special case of hyper-resolution (see [R]). Under the conditions of the theorem, positive literals are either of the form P(c, ... ,c'), or of the form f(c, ... ,c')=c''. The current set of unit clauses is denoted by Us. Anticipating the generalization in Sec- tion 5 the formulation of the algorithm is slightly more general than necessary: "EQ U Us is consistent'' simply says that we do not have f(c, ... ,c')=c; E Us and f(c, ... ,c')=cj E Us with i=/::j, and "c-atom X is implied by IA U lfs" is the case if either XeU80 or X is of the form f(c, ... ,c')c;) and we have f(c, ... ,c')=cjEUs with 0 ~ cjc;). (* generation of unit clauses *) lfs :={At,·· -,Aj}; Unew := {}; REPEAT Us:= UsU Unew; Unew := {}; IF EQ U Us is consistent THEN FOR each clause c-:-1 v · · · vc-:- vD-:t-1, 1,n; 1 DO cancel all C;"J such that Cij is implied by IA U Us; IF all negative literals of the clause are cancelled THEN Unew := UnewU{Dt} OD UNTIL 10 (* test if the unit clauses form a model *) IF EQ U Us is consistent AND there exists no clause Bi:1 V · · • V Bi:m; such that all B"/j are implied by IA U Us THEN f is consistent ELSE f is inconsistent The algorithm terminates since the number of literals is strictly decreasing. By the cancellations the explicit axioms of f are transformed into an equivalent set of Hom clauses. The consistency in the THEN-part can be seen as follows. First note that EQ U Us is consistent. Secondly, every clause not in Us contains a negative literal L - whose complement L + is not implied by IA U Us. It can happen that IA UUs implies L - (for example f(c)=2EUs, L - =-,f(c)c 1 is equivalent to /(c)=c 2 V f(c)=c 3 , which enables a similar construction as in the third paragraph of 4.2. 4.3.3. In view of condition (1), occurrences of notsame (o,a,v> in the antecedent of a rule can be problematic, since negative conditions in a rule result in positive literals in the clausal form. This problem can be overcome by postponing the consistency test until these occurrences evaluate to either TRUE or FALSE (e.g. after querying the user). Then the knowledge base can be transformed into an equivalent knowledge base satisfying (1). An alternative would be to allow clauses with more than one positive literal and to apply the following lemma. Of course the consistency test then becomes in gen- eral NP-hard, the worst-case time complexity doubles with every application of the lemma and we can only hope that practical cases are not the worst. 11 LEMMA. Let r be an axiomatization of an indexed propositional expert system. Let furthermore, for some c-atom A, r 1 be obtained from r by omitting (an arbitrary number of) explicit axioms which are in clausal form (not necessarily Horn format) and contain A as positive literal, and f 2 by deleting A from (an arbitrary number of) such axioms. Then we have: r is consistent if and only if {A } Ur 1 is consistent or r 2 is consistent. PROOF. As to the if-part we remark that {A}Uf1 1= rand f 2 1= r. As to the only-if-part, note that for every many sorted structure~ either ~A or 1=~.A. So if~ is a model of r then~ is either a model of {A} Uf1 or of f 2 , by the definition of fi. f 2 • 0 4.3.4. In our opinion the domain closure axiom is realistic in many applications (apart from the fact that every computer is a finite automaton). The lemmas 3.4-3.8 essentially depend on it. However, Theorem 4.3 remains valid when the domain closure axioms are removed from EQ. For, detected con- tradictions do not depend on the domain closure axioms and, conversely, consistency with the domain closure axiom trivially implies consistency without it. 4.4. Let us briefly discuss the semantical consequences of the conditions (2) and (3) from the previous theorem, since they may slightly deviate from the intended meaning of the knowledge base. It is possi- ble that the consistency of r essentially depends on the valuation f(c, ... ,c')=undefined, i.e. that any valuation f(c, ... ,c')=c; (l:s;;;i:s;;;n) would not yield a model for r. One could say that j(c, ... ,c')=undefined possibly saves the expert system from inconsistencies by preventing production rules with occurrences of f(c, ... ,c') in the antecedent from firing. Since such rµles have obviously not been used in the inference, this may be considered an advantage. On the other hand, this may be con- sidered a disadvantage in cases where f(c, ... ,c')=undefined is not realistic (e.g. temperature (patient) = undefined). In these cases we suggest to add the appropriate unit clause f(c, ... ,c')=c; and to test consistency again. 4.5. Conceptually speaking it is not difficult to generalize the algorithm from 4.3 to universally quantified expert systems, although some care has to be taken in quantifying x in clauses containing literals of the form -,f(c, ... ,c')=x. In these cases only restricted quantification of the form 'r/x=j=undefined is allowed. Of course, the algorithm from 4.3 can become very inefficient (from P(c0), P(c 1), -,P(xi)V · · · V-,P(xn)VQ(xi, ... ,xn), for instance, 2n instances of Q are generated), so we suggest limited use of variables (or, preferably, the use of a more efficient algorithm). 4.6. Ex.AMPLE. We demonstrate the consistency test in action on the case of 1.2. Taking into account the object tree (sub-objects, single/multivalued attributes) the three rules yield the following clauses in shorthand: -,C(p,cp )V P(p,c ), -,f ahdp(p)= yesV-,f char(p,pa)=coV-,P(p,c), -,C(p,ap)V f abdp(p)= yes,-,P(p,c)v f ahdp(p)= yes. When we add the unit clauses C(p,cp) and fchar(p,pa)=co, the empty clause is easily derived and the algorithm decides to inconsistency. If we only add C(p,cp ), then the algorithm decides to consistency on the basis of the following (truth-)valuation: C(p,cp)=P(p,c)=TRUE, C(p,ap)=FALSE, f aMp(P )=yes, fchar(p,pa)=undefined 12 5. ExPRESSIONS 5.1. The extension of the notion of indexed propositional expert system we discuss in this section aims at supporting arithmetic. We start with a real-life example, again taken from HEPAR. A simi- lar example can be found in [BS], pg. 297. greater _than This example shows an extension of the object-attribute-value representation by allowing attribute expressions instead of only attributes. A straightforward extension of the interpretation of tri- ples into many-sorted predicate logic yields the following atom in shorthand: ((tb(b )-db(b)))!tb(b ))* 100>60 In order to capture attribute expressions, the notion of indexed propositional expert system has to be extended. To this end we add new function symbols, called operators and denoted by op,·+, ... , to our language. Moreover the implicit axioms are extended with the positive diagram of each operator op, i.e. with all defining equations op(c;, ... ,cj) = CJ(i, ... ,j) , where the constants are assumed to be of the sort that is required by the type of op. Here f does not belong to the language but denotes a function of indices describing the definition of op. Like = and <, operators are provided by the system. Let OP denote the set of axioms for operators. A typical example of an operator is addition of integers, denoted by + and written as an infix operator. From now on IA will denote EQ U 0 U OP. 5.2. We now extend the notion of c-atom as defined in Section 3 in the following way: a c-atom is a closed atom of the form P(c, ... ,c') or of the form: expression relation symbol expression Here a relation symbol is one of the symbols < , = , > and an expression is a term built up from constants and terms of the form f(c, ... ,c') by applying the operators (respecting types and sorts). 5.3. From now on indexed propositional expert systems as defined in 3.1 are understood to be extended in the sense of 5.1 and 5.2 above. In order to be able to carry over Theorem 4.3 we intro- duce the following definition. DEFINITION. Assume every sort has a constant undefined as stated above in the conditions (2) and (3) of Theorem 4.3. An operator op is called strict if the implicit axioms for op satisfy the following condi- tion: op(c, ... ,c')= undefined if one or more of the arguments c, ... ,c' equals undefined. Note that for a strict multiplication * of integers we have O* undefined = undefined and not O* undefined = 0. 5.4. THEOREM. Let r be an axiomatization of an indexed propositional expert system satisfying the con- ditions ( 1)-(4) of Theorem 4.3 above. Assume moreover that the following conditions hold: (5) Every operator is strict and takes polynomial time. ( 6) No operators occur in the positive literals occu"ing in the explicit axioms of r. (7) All equations occu"ing in negative literals in the explicit axioms of r are of the form expression = c. Then the consistency of r can be tested in polynomial time. 13 PROOF. Due to its general formulation, the algorithm from 4.3 carries immediately over to the present case. However, the argument demonstrating the correctness of this algorithm is slightly more compli- cated, and needs to be restated in some detail. We first note that the evaluation of expressions (such as the example in 5.1) may require more than one unit clause (both the values of tb(_b) and db(_b) are necessary). Furthermore, under the conditions (4) and (6) of the theorem, positive literals are of the form P(c, ... ,c'), f (c, ... ,c')=c", f (c, ... ,c')= g(d, ... ,d'), or c =c'. The latter kind of literals evaluate immediately to TRUE or FALSE (by using EQ), so we may assume without loss of generality that they do not occur in the explicit axioms of r. Moreover, under condition (7) of the theorem, negative literals are essentially of the form -, P(c, ... ,c'), .., expression I < expression2 or .., expression =c. By this more general form of literals involved, as well as the fact that IA = EQ U 0 U OP instead of IA = EQ U 0, the statements "EQ U Us is consistent" and "c-atom X is implied by IA U Us'' have a more general meaning than in 4.3. For example, the former statement now also excludes f(c)= l,f(c)= g(d),g(d)=2E'Us, whereas the latter holds for X the c-atom from 5.1, with -, I, *and > having their usual meaning axiomatized in IA, and tb(b )= 100,db(b )= 39E Us. The consistency in the THEN-part follows from the following (truth-) valuation: { TRUE if P;EUs P; = FALSE otherwise { c if EQU Us t: tj=c tj = undefined otherwise Again we have that EQ U Us is consistent and that every clause not in Us contains a negative literal L - whose complement is not implied by IA U Us. It can happen that IA U Us implies L - (for exam- ple L - = -,f(c)+ f(c')