Semantic Resolution for Horn Sets

I. Introduction

Since the introduction of resolution for automated theorem proving, one line of effort has been to develop strategies and hueristics for special classes of clause sets or special classes of j)roblems. One such cla'ss is the class of Horn sets. Recent interest in Horn sets [3,6] stems from the fact that many strategies that are not complete in general are complete for Horn sets. For example, positive unit resolution, which for Horn sets is just Pl resolution, is complete. Negative resolution is just set-of-support resol­ ution with the set of support the negative clause. Factoring is not necessary in order to refute an unsatisfiable set of Horn clauses [3]. In addi­ tion to possessing many useful and interesting properties, Horn sets occur quite often in prac­ tice. For example, the axiom systems for groups, rings, and many other algebraic systems have Horn sets as the natural translation into clause form as do various formal systems (see e.g., Hermes [4]). Horn clauses also have a great deal of intuitive appeal, for the Horn clause -L~V ··· v -~VM is logically equivalent to (L 1 A ··· Lk)--lM. That is a Horn clause represents an implication in which each of the antecedents is a positive unit (or intuitively, a simple statement of fact or hypothesis) and the consequent is also a posi­ tive unit. Many mathematical axioms and theorems take this form. Finally, one can apply the split­ ting techniques developed in [3] to reduce a non-Horn set of clauses to a class of Horn sets; thus, the theory developed for Horn sets can be applied indirectly to non-Horn sets as well. The purpose of this paper is to present a new strate­ gy (essentially a sharpening of semantic resolu­ tion) that is complete for Horn sets and to dis­ cuss some interesting properties of Horn sets that greatly simplify the implementation of semantic resolution for those sets.

While many methods for resolution are com­ plete for Horn sets, some desirable combinations of strategies are not complete together even when the class of problems is restricted to Horn sets. Two such strategies are positive-unit resolution

and set-of-support resolution [3] . Restricting

Lawrence J. Henschen Northwestern University Evanston, Illinois

resolution to unit resolution avoids the combina­ torial explosion of the number of clauses gener­ ated on the various levels that is usually present when non-unit resolution is allowed. For, in the latter case, when forced into the non-unit section of a theorem prover, a program usually must try resolution on all pairs of literals from a pair of non-unit clauses. (When ordering or lock resolution [2] is used this is not the case; however, these methods are not compatible with many of the more successful strategies like set of support.) Thus, once the program leaves the unit section, even for just one level, relatively large numbers of resolvents are generated. Then in developing a strategy that is not compatible with unit resolution, great care must be taken to control the non-unit resolvents that are allowed to be generated lest the combinatorially explosive non-unit section undo the savings that the strategy yields in the unit section. Of course, semantic resolution [2] has as its main goal to restrict the resolvents· generated to those that are highly likely to be relevant to the proof by taking into account the intended meaning of the clauses. In semantic resolution, an interpreta­ tion I of the symbols of the language is input to the theorem prover along with the set of clauses to be refuted. Then one parent in each resolution is required to be false in I. The idea is that two clauses which are both true are less likely to produce a deduction leading to a contradiction than are two clauses one of which is false. The most widely-used special case of semantic resolu­ tion is set-of-support resolution in which the interpretation I satisfies just the axioms and is only implicitly present. In Section 2 we develop a strategy which is a combination (but not the intersection) of positive-unit resolution and semantic resolution.

One difficulty with semantic resolution is that if the domain of the interpretation contains more than a few elements the computation required to fully evaluate a non-ground clause may be too time consuming. In addition there is a problem of how to represent for each clause the sets of domain elements for which the clause is true and those for which the clause is false. For these reasons, most applications of semantic resolution have used only very simple interpretations; for example, the interpretation in which all literals are false yields Pl resolution. In Section 3 the problem of reducing the amount of computation and storage required for evaluating Horn clauses based on the use of cross products of interpre­ tations will be discussed. Section 4 will contain some concluding remarks.

II. Completeness of Positive-unit Semantic Resolution for Horn Sets

The reader is assumed to be familiar with the resolution principle for first order logic and the terminology related to it. The defini­ tions necessary for the particular theorems to be proved will be presented; then some lemmas will be recalled and the completeness of the strategy proved.

DEFINITION: A Horn clause is a clause containing not more than one unnegated literal. A Horn set is a set of Horn clauses.

DEFINITION: An interpretation I for a set S of clauses consists of a non-emoty domain D of objects and an assignment of the predicate, func­ tion and constant symbols occurring in S such that each n-ary predicate symbol is assigned an n-ary relation on D, each n-ary function symbol is assigned an n-ary function on D into D, and each constant symbol is assigned an element of D.

In the standard inductive way the assignment of values to symbols in S can be extended to an assignment of all ground formulas over the alpha­ bet of s. If~ is the assignment above, define ¢ 1 as follows: let¢ 1 · ¢ on the predicate, function and constant symbols of S; let ¢ 1 (f(t 1 , ··· , tn)) be ¢(f)[¢ 1 (t 1 ), ··· ,¢ 1 (tn)] for the ground term f(t 1 , ··. ,tn) and ¢ 1 (P(t 1 , ··· ,tn)) be ~(P)[¢ 1 (t 1 ), ··· ,¢ 1 (tn)] for the ground atom P(t 1 , ··· ,tn); and let ¢ 1 interpret the logical connectives according to their usual meaning.

DEFINITION: A clause is falsified by the inter­ pretation I if it has a ground instance which is falae in I.

DEFINITION: A clause is positive if it contains only unnegated literals. A clause is negative if it contains only negated literals. A clause is mixed if it contains both negated and unnegated literals.

DEFINITION: A unit is a clause containing one literal.

DEFINITION: A resolvent of two clauses A and B is a positive-unit resolvent if one of A and B is a positive unit. A positive-unit refutation of a set S of clauses is a refutation in which each resolvent is a positive~unit resolvent.

DEFINITION: Given an interpretation I, a resol­ vent of two clauses A and B is a semantic resol­ vent with respect to I if one of A and B is falsified by I. A refutation of a set S of clauses is a semantic refutation with respect to I if every resolvent in the refutation is a seman­ tic resolvent with respect to I.

In [3] it was shown that any unsatisfiable Horn set has a positive-unit refutation but that for an ·arbitrary set of support, T, there may not be a !-supported positive-unit refutation. That is, the intersection of the two strategies, positive-unit resolution and set-of-support re­ solution, is not complete for the class of Horn sets. Since set-of-support resolution can be viewed as a special case of semantic resolution [2], it follows that the intersection of positive­ unit resolution and semantic resolution also is not complete for the class of Horn sets. Now, semantic resolution is an attempt to bring the meaning of the symbols into the search effort as an aid in guiding a program to the generation of the empty clause, the idea being that in order to generate the contradiction that produces the empty clause, i.e., falsehood, one should use clauses that are themselves false. Positive-unit resolution has as its goal the elimination of a class of resolutions that produces combinatorially large numbers of new clauses. In addition, there is an intuitive appeal to positive units as con­ veying more information than other clauses since it is generally more useful to know that a parti­ cular property holds than to know just that one of a number of statements hold (see [3] for a more complete discussion of the advantages of unit resolution). A strategy that was based on both of these intuitively appealing ideas would seem to be a good candidate for an efficient theorem prover for Horn sets. Since the intersection of the t)'O cannot be complete conditions must be relaxed and/or altered in such a way as not to lose the advantages of the two constituent strategies. In particular, relaxing the conditions to allow non-unit resolution must be done with extreme care.

In the strategy presented below, this rate of growth will be controlled by requiring that for non-unit resolutions one parent and the resolvent both be falsified by the interpretation. Since the number of false resolvents generated by a false clause will generally be smaller than the total number of resolvents that the false clause could generate, this new restriction should cut down the number of clauses that will be generated by non-unit resolution. With this restriction on the non-unit section, an additional restriction can be placed on the positive-unit section -­ namely, that the positive unit must be false. The net effect of these modifications is to produce a strategy that combines the advantages of positive-unit resolution and semantic resolution and that relies especially heavily on the seman­ tics, provided by the user in the form of an interpretation, to guide it through the dangerous non-unit section. Also, if the interpretation does not falsify any axiom, as would be the usual case, then as in set-of-support pairs of axioms will not be allowed to resolve directly even when one of them is a positive unit, a short­ coming of just positive-unit resolution (and indeed, of hyperresolution in general). Finally, the reader may also note a great similarity between the method used in the completeness proof here and of bilinear resolution of Kuehner [6]. There, of course, there is no restriction on positive-unit resolution. Also the non-positive­ section of a bilinear program is based purely on syntactic considerations, i.e., on the use of negative clauses.

Before proving the completeness of the new strategy, some previously proved results [3] on Horn sets are recalled and some lemmas are proved. The ground case is considered first. The following two lemmas from [3] are recalled.

DEFINITION: A set S of clauses is minimally unsatisfiable if S is unsatisfiable but no proper subset of S is.

LEMMA 1. (LEMMA 1 from [3]) If S is an unsatis­ fiable set of Horn clauses then there is a LEMMA 2. (THEOREM 5 from [3)) If S is a minimal­ ly unsatisfiable set of Horn clauses, then S contains exactly one negative clause.

One additional lemma is proved before the completeness theorem is given.

LEMMA 3. Let S be a minimally unsatisfiable set of ground Horn clauses, and let p be an atom occurring in S. Then p occurs unnegated exactly once.

PROOF. Of course if p occurs in S it must occur positively at least once or -p would be a pure literal, and S would not be minimally unsatis­ fiable. Now suppose S contains the clauses pAl,pA2, ··· ,pAn; -pB1,-pB2, ··· ,-pBm; cl,c2, ···· ck

where all occurrences of p and -p are shown explicitly. Then s 1 = (A 1 , ··· ,An,c 1 , ··· ,ck} is also unsatisfiable. Moreover, since each clause pAi is a Horn clause and p is an atom, each Ai is negati~e. Now if any Ai is empty, then p occurs in S as a positive unit and subsumes any other clause that contains the positive literal p. In this case, if n>l, S cannot be minimally unsatis­ fiable. If no Ai is empty and n>l, then by LEMMA 2 above, s 1 is not minimally unsatisfiable for it contains more than one negative clause. Let s 2 be minimally unsatisfiable subset of S and let A be the one negative clause from s 1 1 that is presen~ in s 2 · (Indeed, one Ai must be present or else a subset of the set (c 1 , .·· ,C} would be unsatisfiable contradicting the minimhl unsatis­ fiability of S.) By returning the literal p to Al, one obtains a deduction of the positive-unit c ause p from the clause pA and the clauses C , ~j~. Having deduced ~his unit clause, all o! the clauses pAi can be discarded because they are subsumed by p and a refutation of S obtained from p and the remaining clauses of s. Thus a refutation exists which uses only one clause con­ taining the positive literal p. But it had been assumed that n>l, and so S could not be minimally unsatisfiable, a contradiction. QED

Of coarse, if S is minimally unsatisfiable but ~ Horn, it may very well contain several occurrences of a positive literal as can be seen by the example (pq,p-q,-pq,-p-q}.

THEOREM 1. Let S be an unsatisfiable set of ground clauses and suppose S is a Horn set. Let I be an interpretation for the language of s. Then there exists a refutation R of S such that each resolution in R satisfies one of the follow­ ing two conditions: 1. one of the resolvends is a positive unit which is false in I, or 2. one of the resolvends and the resolvent are both false in I.

PROOF. The ·proof proceeds by induction on the number n of atoms occurring in S. It may be assumed without loss of generality that S is minimally unsatisfiable.

Case 1. n·l. In this case S consists of the two unit clauses p and -p. One of the two clauses is false in I and the resolvent, namely the empty clause is false, so that the one step refutation satisfies condition 2.

Case 2. Assume that the theorem holds for all sets of clauses containing less than n atoms, and suppose S contains exactly n atoms. There are two subcases.

Subcase a. S contains a positive unit p which is false in I. Let S consist of the clauses p, -pB 1 , ··· ,-pBk,c 1 , ··· ,cm. Since pis a false positive unit, each resolution R(p,-pBi)·Bi satisfies condition 1 of the theorem. By LEMMA 3, no other clause of S contains the positive literal p. Thus from S by a sequence of resolutions satisfying condition 1 one can gener­ ate the set of clauses s 1 =(B 1 , ··· ,Bk,c 1 , .·· ,cm}.

s 1 is unsatisfiable and contains strictly fewer tfian n atoms. Thus by the induction hypothesis there is a refutation R of S satisfying the conditions of the theorem. tnen the juxtaposition of the k resolutions involving p and R also satisfies the conditions and is a refutation of s.

Subcase b. S contaiDs no positive units which are false in I. (The reader may wish to consult Example 1 below while reading this por­ tion of the proof.) By an iterative process we will locate a false clause in S which can be used to start a sequence of resolutions satisfy­ ing condition 2; that is, each resolvent in the sequence will be false. Finally, the last resolvent will either be the empty clause or a false positive unit. Now, from LEMMA 1 one can conclude that S contains at least one positive unit clause. Let the positive units of S be p 1 , ··· ,pn 1 · Form the set s 1 by excluding these positive units from S and deleting the literals -pi' ~~n from the remaining clauses. In the usual way bne can establish that s 1 is unsatis­ fiable and Horn. If s 1 does not contain a false positive unit or the empty clause then let p + 1 , ··· ,p be the positive units of s 1 · Form nl n2 the set s 2 by excluding from s 1 these positive units and deleting the literal§ -pi,n 1 +~~ 2

from the remaining clauses. As above s 2 is unsatisfiable and Horn. Continue generating sets Si, at each step excluding the (true) positive units and deleting their negations from the other clauses, until an S is obtained which contains either a false posi!ive unit or the empty clause. Note that since each pi is a true positive unit, each negative literal Ehat was deleted from a clause in the above process is false. Now suppose that Sm contains a false positive unit, say u. This positive unit corresponds to a clause U=-q 1 -q 2 ··· -qju in S where each qg is one of the ph' ~m that was deleted in forming the Si's. In addition each pi' lSi~m corresponds to a similar clause Ci in s. Also note that U is false in I since u is false in I and each -q is the negation of a true positive unit; in thejsame way each negative literal of each Ci is false in I. We have now located the desired false clause, u. A chain of resolutions beginning with U, using the Ci and satisfying condition 2 will now be given that will generate the false positive unit u. The clause U contains a literal which is the negation of a positive unit that was excluded in producing Sm from Sm-l" That unit pi in

Sm-l corresponds to clause Ci in s. The resol­ vent of U and Ci on pi consits of the positive literal u and some negative literals from among the -p . But each of these literals is false so that t~e resolvent of U and C , call it D , is false in I. Therefore, this ~esolution sWtlsfies condition 2 of the theorem. If D 1 contains another literal, say-p with n 1 ~j~ (i.e., a literal that was elimiAated inmforminW the last set S ) form the resolvent D 2 using D 1 and C · m m, m, j As above, Dm 1 and Dm 2 are both false, so condi­ tion 2 is satisfied. 'Continue in this way until all negative literals that were deleted in forming Sm from Sm-l have been resolved away. Call the resulting c ause D . Note that each negative literal in a clausW Ci where n 1 <iSn corresponds mm to a literal Sk, kSnm-1" that was eliminated in forming an Thus, not only is Dm false in I and contains the positive literal u, it contains only negative literals that were deleted i.n forming sets Sk with k<m. The above process is now repeated resolving away negative literals from D that correspond to literals that were eliminated in forming S 1 from S 2 · Call the mmresult of this step Dm_ 1 . As above Dm-l is false, contains thr positive literal u and does not con­ tain a negative literal that participated in forming either S _ 1 or Sm. Continue in this way until the clausemo 1 is formed. Indeed, o 1 is just the positive unit u which is false in I. More­ over, since u is present in each resolvent in the sequence, all the intermediate resolvents and U itself can be discarded by subsumption once u is generated. That is, (S-lU})Ulu} is unsatisfiable. Now the false positive unit u can be used to eliminate the literal u altogether as in Case a above; the result is an unsatisfiable Horn set that contains fewer than n atoms. The induction hypothesis now gives the desired result. In case Sm contains the empty clause, the above process can be used with the only modification being that each of the intermediate clauses does not contain a positive literal and the final clause o 1 is the empty clause; thus when the process terminates, the result is in fact a refutation all of whose resolutions satisfy condition 2 (see Example 2).

This completes the induction step and hence also the proof of the theorem.

The process in the proof of Theorem 1 will now be illustrated with two examples.

EXAMPLE 1. Let S be the set of clauses lr,-rq, -rs,-q-sp,-pt,-t} and let I be the interpretation that assigns the value true to r, q, and s, and false to p and t. Now r is the only positive unit in S and it is true. According to the proof of the theorem the set s 1 a(q,s,-q-sp,-pt, -t} would be formed. Then ~ince both the positive units occurring in s 1 are true, the process in the proof would continue to find the set s 2 =lp,-pt,-t~ s 2 does contain a false positive unit,p. Therefor~ according to the proof, the clause -q-sp of the original set S could be used to start a chain of resolutions that would result in the false posi­ tive unit p. One would first form the resolvent of -q-sp with, say, -rs to get the clause -r-qp. Note that -q-sp is false and that the resolvent -r-qp is also false and that the only true literal of the clause -rs is the positive literal s. Now the resolvent of -r-qp and -rq is formed. This resolvent is· -rp which is also false. Finally, the resolvent of this clause and the clause r is generated. This last resolvent is the positive unit p, which is a false positive unit clause. This can now resolve with -pt to produce the clause t. This clause resolves with the unit -t to produce the empty clause. Note that a theorem-proving program would not, of course, actually generate the sets s 1 and s 2 ; they were discussed here only to illustraEe the process of the proof of Theorem 1. A program would simply note that the clause -q-sp was false and that the resolvent of -q-sp and -rq was also false and therefore legal to add to the set of generated clauses. Note that since literals -pi might be deleted from several clauses in forming the Si sets, one might expect a considerable amount of merging. However, the strategy cannot be strengthened to require merging as can be seen by noting that if the false clause U has only 2 literals, its resolvent with another Horn clause cannot be a merge.

EXAMPLE 2. Let S be as in Example 1, and let the interpretation I assign the value true to all atoms. The process in the proof of the theorem would generate sets s 1 and s 2 as in Example 1. However, the positive unit p of s 2 is not false for this I. Thus the set s 3 =lt,-E} would be generated. This set also does not contain a false positive unit so the set s 4 =lempty clause} would be generated. Now the empty clause comes from the clause -t in s 4 · As above one would start with this clause and work back, resolving first with the clause -pt to produce -p, then resolving with -q-sp to produce -q-s and so on. Again, an actual program would not consider any of the sets s 1 -s 4 , but simply which clauses were false and had false resolvents. Note that when the interpretation makes all atoms true the refutation produced will be an Nl refutation, and that for Horn sets, such refutations are also input refutations [3].

It is now shown that Theorem 1 does not remain true when the condition of being Horn is removed. Let S be the set (pq,-pq,p-q,-p-q} and let the interpretation I assign true to both p and q. Then one can generate resolvents using the false clause -p-q producing the two clauses -p and -q. However, neither of these can resolve with the clause pq since neither is a false posi­ tive unit and in each case the resolvent is not false. Thus no refutation can be produced satisfying the .conditions of Theorem 1. Indeed, there is no refutation even if condition 1 is relaxed to read one ancestor is a false positive clause instead of unit. This set of clauses can also be used to show that the converse of Theorem 1 is not true. Let I assign both p and q false. Then the clause pq is false and its re­ solvent, p, with -qp and its resolvent, q, with -pq are both false positive units so that these resolutions satisfy condition 2. These false positive units can be used one after the other to produce the empty clause from -p-q. However, S is not a Horn set and indeed no renaming of S is Horn. We do have the following result, however.

THEOREM 2. Let S be a set of ground clauses which is minimally unsatisfiable. If for every interpretation I there exists a refutation satis­ fying the conditions of Theorem 1, then S is Horn PROOF . Suppose S contains a non-Horn clause, say C=pqC', where p and q are two positive literals. Let I be an interpretation in which both p and q are true. Now consider any refutation R of S. Since S is minimally unsatisfiable, C must occur in R. Wherever C enters R the literals p and q will enter and will propagate until one of them is resolved away. Suppose p is the first of the two from C to be used as a literal of resolution. Now the clause resolving on p with C or its descendent must contain the literal -p and therefore certain­ ly cannot be a false positive unit. Of course, the resolvend containing p and q also cannot be a positive unit. Thus condition 1 cannot be satis­ fied. Next, the resolvent must contain the posi­ tive literal q, which is true in I. Thus the resolvent cannot be false and condition 2 cannot be satisfied. Therefore R cannot satisfy the conditions of Theorem 1. Since R represented an arbitrary refutation of S we have a contradiction to the hypotheses of this theorem.

It should be pointed out that the conclusion of Theorem 2 is that S is Horn, not just that some renaming of S is Horn. Indeed, if a set S has a renaming which is Horn but S itself i:; not Horn, then S will have an interpretation I as in the theorem relative to which there is no refutation satisfying the conditions of Theorem 1.

THEOREM 3. Let S be an unsatisfiable set of Horn clauses. Let I be an interpretation over the language of S. Then there exists a refutation R of S auch that each resolution in R satisfies one of the following two conditions: 1. one of the resolvends is a positive unit which is falsified by I, or 2. one of the resolvends and the resol­ vent are both falsified by I.

PROOF. Let S' be an unsatisfiable set of ground instances of clauses in Sand let R' be a refuta­ tion of S' satisfying the conditions of Theorem 1 with I as the interpretation. Let R be the refuta­ tion of S obtained by lifting R' in the usual manner. R satisfies the conditions of this theorem as can be seen by the following. Suppose p is a false positive unit in R' and P is the correspond­ in& clause in R. P cannot contain a negative literal because it has a positive clause, p, as an instance. Also, P cannot contain more than one positive literal because it is either in a Horn set or is deduced from a Horn set by resolution [3]. Thus P is a positive unit. Moreover, it has p aa an instance, and p is false in I. Therefore, I falsifies P, and the resolution in R using P satisfies conditon 1 of this theorem if the corres­ ponding resolution in R' using p satisfies condi­ tion 1 of Theorem 1.

In a similar way, if a resolution in R' satisfies condition 2 of Theorem 1, the corres­ ponding resolution in R will satisfy condition 2 of this theorem because one of the resolvends and the resolvent will have instances which are false in I. Since every resolution in R' must satisfy one of the two conditions, the theorem is proved.

Ill. Implementation

While semantic resolution has a great deal of intuitive appeal, in actual practice few theorem­ proving me thods that have been programmed use any but the most trivial of interpretations for the languages being used and they arc usually based on some syntactically recognizable feature. For example, the underlying interpretation for Pl resolution and also for hyperresolution is the interpretation in which every predicate symbol is assigned the relation which is identically false, and false clauses are recognized by : the lack of negative literals. One would like to see the use of interpretations which satisfy, say, the axioms of the mathematical theory under consideration and thus would have the effect of focusing atten­ tion on the special hypotheses and conclusion of the result for which a proof is sought, as in set-of-support resolution. The advantage here over just set of support would be that the seman­ tic requirement, i.e., that one ancestor be false, would have effect at all levels of the ·search whereas set-of-support resolution, while quite effective at level 0, allows any level 1 or greater clause to resolve with any other clause. Or perhaps even better, one would like to be able to arrange the interpretation so as to single out particular clauses as being important for the particular theorem by making those clauses false in the interpretation even if some do happen to be axioms. That is, for a particular problem the user might suspect that a certain axiom was especially relevant; he could arrange that axiom to be false in the interpretation thus allowing it to enter the semantic search at an earlier stage.

There are two reasons why little use has been made of semantic information in theorem provers. First, for interpretations whose domains are not fairly small, determining whether or not a clause containing variables is falsified may be a formidable job. For example, the stan­ dard pair of axioms for associativity in group theory each have 6 variables. In a domain of 100 individuals, the determination that one of these axioms has no false instagce, the normal case, would require testing 100 different 6-tuples. Even with highly efficient, optimized methods such a task would not likely be feasible. The second reason has to do with representing, for a given clause, which values falsify that clause. That is, having determined whether a clause possibly has some instances which are false, one would like to save that information. If a clause C has several variables, there may be many tuples that falsify C requiring more storage to save than the information might be worth. The purpose of this section is to present methods by which these two problems might be overcome. These remarks are not meant to be an exhaustive study of this area; in particular, this section will not discuss in great detail the methods and data structures that might be used by a particular program. Rather the purpose is to present some interesting, previously known results about inter­ pretations and Horn sets and to indicate briefly how these properties can be useful for theorem­ proving programs. We begin with a basic defini­ tion from mathematics.

DEFINITION; Let L be a first order lan&uage, and let I 1 and I 2 be two interpretations over L with domains o 1 and o 2 respectively. The cross-product of I 1 and I 2 is the interpretation I whose domain Dis the cross-product of D and D (i.e., the set of ordered pairs whose first coordfnate comes from D 1 and whose second coordinate comes from D ) and wnich assigns values to the predicate, constant, and function symbols of L as follows: if a is a constant symbol and I 1 assigns a to a and I assigns a 2 to a, then I assigns ~he ordered ~air (a 1 p 2 ) to a; if f is an n-ary function symbol and if Il assigns to f the n-ary function f on o and 2 assigns to f the n-ary function 1 f oh D then I assigns to f the n-ary function on t x o 2 ' which maps ann-tuple of ordered pairs (ta ~b ), 2 ... ,(a ,p )) onto the ordered pair 1 1

n n

(f 1 (a 1 , ··. ,an),f 2 (b , .·. ,bn)); if pis a predi­ caEe symbol and If \ 1 assigns to p the n-ary predicate P 1 on o 1 and 1 2 assigns to p the n-ary predicate P 2 on o 2 , then I assigns to p the n-ary predicate wnich is true for an n-tuple of ordered pairs ((a 1 ,b 1 ), ··· ,(a ,b)) if and only if both P 1 (a 1 , ·.. ,an} and P 2 (R 1 ,? ·· bn) are true.

McKinsey [7) noted that if a clause con­ taining only one positive literal is true in two interpretations then it is also true in the cross product of the two interpretations. In addition, if a clause C is true of each algebra in a class of algebras that is closed under algebraic direct product, then there is subclause C' of c contain­ ing at most one positive literal (i.e., c· is Horn) and C' is also true of every algebra in the class. Horn [5) later showed that the class of Horn sets and the class of sets of clauses which are true in a direct product of two interpretat­ tions if and only if they are true in each indi­ vidual interpretation are the same class. (Thus the name Horn clause.) In both cases only clauses containing only the equality predicate were con­ sidered; however, their methods easily generalize. Some of these results will be reviewed in the following paragraph; the reader is referred to [7) and [5) for the full presentation of this material as well as other results.

Consider two interpretations I and I and a ground literal L. If Lis an atom, 1 then b~ definition L is true in I 1 x 1 2 if and only if it is true in both I 1 and I 2 · Now if L is the negation of an atom, say L=-M, then L is true in I 1 x I 2 if and only if it is true in at least one of I 1 and I 2 . For M i~ true in I x I if and only if it Is true in both I and 1 I 2 , ~nd so M is false (i.e., Lis true) i! and only if M is not true in both I 1 and I 2 , that isM is false in at least one of tnem. Next, suppose the ground Horn clause Ca-1 1 ·.· -L M is true in both I and I · Now if M is true Yn both I 1 and I theh M is true in the cross-product, and so C is 2 also true in the cross-product. If M is not true in one of the I's, say M is false in I 1 , then some negative literal -Li is true in I · By the above, -L is true in the cross-produc~, so again C is tru~ in the cross-product. Thus, any ground Horn clause that is true in two interpretations is true in the cross-product. Of course, a Horn clause would be false in I 1 x I 2 if and only if each neg­ ative literal was false In both I and I and the positive literal was false in at least o~e of the two. This analysis applies equally well to the case of determining if a particular instance of a clause with variables is true or false in the cross-product of two interpretations. These results generalize to products of more than just two interpretations in a straightforward way. Thus, if I 1 , . · . ,I 0 are interpretations and Cis a Horn clause which is true in each I , then c is true in I 1 x ··· xin. If Cis false ih I x ··· xi then each negative literal of C is fal~e in egch Il and the positive literal of C is false in at 1 ast one Ii.

The above remarks form the basis for reduc­ ing the amount of work required to evaluate Horn clauses for semantic resolution and to store in­ formation about the tuples for which such clauses are false. Consider again the case of an assoc­ iativity axiom C with 6 variables. If instead of a single interpretation with a domain of 100 ele­ ments we use the cross-product of two interpreta­ tions each of whose domains has 10 elements (and thus whose cross-product domain has 100 elements), then to evaluate C in I 1 x I~ gne would evaluate C in I 1 and I 2 requiring 2*~0 y 2 tuples to be considered as oppos~d to 100 =10 , with a reduc­ tion factor of 5*10 · If more subinterpretations are used the savings is even more dramatic. For example, by using three domains each with 5 ele­ ments, we would be using the equivalent of a single interpretation whose domain had 125 ele­ ments, and the evaluation of a clause with 6 var6ables would require the 4 consideration of 3*5 , or approximately 5*10 , 6-tuples. Moreover, efficient means of organizing the calculations can be expected to reduce to an even greater degree the number of tuples requiring testing for a given clause.

The storage problem can also be reduced by taking advantage of the properties of Horn clause~ For the purposes of this paragraph we use the following notation:

if a=(al, ··· ,an) and b=(bl, ··· ,bn) are two n-tuples then a X b Will indicate the n-tuple of ordered pairs ((a 1 ,b 1 ), ··· ,(a ,b)), Recall that a clause C is false In I x In i~ and only if every negative literal i~ fal~e in both I and I and the positive literal is false in at l~ast on~ of the two subinterpretations. The amount of space required to store the set of tuples falsi­ fying a clause in the cross interpretation can be greatly reduced by storing instead certain tuples from the subinterpretations and using these to construct tuples from the cross interpretation when (and if) needed, Suppose the tuples of values that make C false in I are a , ··· ~a and those that make C false in I 1 are b ! ... ,b? Further, suppose the tuples that make all mthe negative literals of C £alse b~t the positive literal true in 1 1 are cl, ··· ,c 1 and those for I 2 are d 1 , ··· ,dm'' Cons der a 0 tuple from Il X I2 of the form ai X z. If z is one of the b' a· - is or is then by the above remarks a x z makes C false n the cross interpretation sifice the first coordinate falsifies every literal of C while the second coordinate satisfies at most 1ust the positive literal. On the other hand if z is not among the b's or d's, then it satisfles a negative literal of·t and ~o ai x z must satisfy C in I 1 x I 2 ._ A ~imilar remark holds for values of the form z x b · Finally, a value of the - - i form ci x d must satisfy C since both c and d satisfy thejpositive literal of C. Also ias j - - , ~bove~ any value of the form z x y where either z or y is not among the appropriate lists must satisfy c. Thus, the tuples of the cross interpret~tion_that falsify Care a 1 X bj, ai X dj, and ci x bj for diffenent comb nations of i and ~ Thu ~ oy saving, in addition to the values in the subinterpretations that falsify the clause, those values that falsify the negative literals but sat­ istfy the positive literal one can significantly reduce the amount of storage required. To get an estimate of the kind of saving involved, consider again two interpretations of 10 elements eac~ and a clause with three variables. There are 10 3-tuples of values in each domain. Suppose a third falsified the clause in each domain and an­ other third falsified the negative literals but satisfied the positive literal. Then there would be 666 triples in each domain that need to be saved or 1332 altogether. In the cross interpre­ tation there are 333*333*3=332667 triples of ordered pairs that falsify the clause. As before, if more smaller domains are u ed, the reduction is even more drastic. Moreover, efficient nota­ tions from set theory can be used to store such information. For example, if several tuples have coordinates in common, this can be indicated by condensing some of the coordinates to be sets. E.g., the six triples (a,b,c), (a,b,d), (a,b,e), (e,b,c), (e,b,d) and ~,b,e) could be represented by ((a,e},b,(c,d,e}). That is, anything from the set (a,e} can be used as first coordinate, b as second coordinate and any of (c,d,e} for the third Such notations have proven useful in other con­ texts in theorem proving (see, for example, Auguston and Minker [ 1]).

Finally, the use of cross-products makes it easier for the user to "tailor" interpretations to emphasize particular clauses by giving the various clauses the appropriate properties in the coordinate interpretations. For examp~e, consider the theorem of group theory that if x ·e for every x the group is commutative and its standard representation as a set of clauses with the con­ clusion negated. This set contains the three units Pxxe, Pabc, and -Pbac. Suppose one would like to concentrate on Pabc and -Pbac and delay the entry of Pxxe into the search. Then in the cross product interpretation Pabc and -Pbac must be false while Pxxe must be true. Then Pabc must be made false in at least one of the interpreta­ tions in the cross-product while the atom Pbac must be true (i.e., -Pbac false) in all the inter­ pretations in the cross product. Also, Pxxe must be true in all interpretations. It would be easier to devise two interpretations of, say, 4 or 5 elements each, that satisfy these conditions, especially the condition on Pxxe, than to verify them for a single interpretation of 20-25 element~ If the above conditions are satisfied and the two subinterpretations are themselves groups, then neither the axioms nor the clause Pxxe can be resolved together, and the refutation search must begin with either Pabc or with -Pbac and another clause whose resolvent with -Pbac has a false instance in the cross-product. Indeed, the clause Pxxe would not be able to resolve with any clause C unless C and the resolvent both had false instances.

IV. Concluding Remarks

This paper has presented a new strategy, a strengthening of sL~antic resolution, which is complete for the class of Horn sets. This strategy is actually a combination of semantic and syntac­ tic approaches--syntactic because the emphasis on positive units is totally independent of any intended meaning of the symbols; semantic because different interpretations supplied by the user will yield different search spaces. The results reviewed in Section 3 will prove most useful in actually implementing the new strategy, or indeed any semantic strategy, for programs that will deal with Horn sets. The time and storage savings that those results will provide may make it possible for the first time to construct truly semantic programs, that is programs which can use the info~ mation provided by the user about the intended meaning of the clauses as opposed to a meaning imposed by some syntactic property as in hyper­ resolution. There are same questions that are raised by these results. First, it may be possible to derive an efficient strategy from Lemma 3 and constrained-variable resolution. Als~ it would be very interesting indeed to know if some version of Theorem 1 held in the non-Horn case for hyperresolution, which is the analogue of positive-unit resolution for Horn sets. · Finally, it would be most useful to know how many of the results here carry over to paramoduiation for equality.