Semantic Paramodulation for Horn Sets

1. Introduction

In [ 19] it is argued that paramodulation has the fol­ lowing advantages over resolution with the equality axioms: 1. paramodulation emphasizes the use of the functional representation as opposed to the relational representation; 2. in functional representation terms are not split up and so demodulation is more effective; and 3. paramodulation works directly on deeply nested terms as opposed to resolution which us es function substitution to build up or tear down terms one level at a time. On the other hand, paramodulation has proven difficult to con­ trol. Some restrictive strategies of a general nature have been developed [e.g., 13, 18], but these are still not as effective as we would like . An often-times useful approach is to consider strategies for special classe3 of problems. In this paper we present a new semantic s tra­ tegy for paramodulation for Horn se ts , extending the work of [ 4]. We prove the completeness of the str ategy and discuss some issues relating to its use (in particular, some ideas about how interpretations should be chosen).

2. Preliminary Theoretical Results

Definition. A Horn semantic resolution with respect to an interpretation I is a resolution inference which satisfies one of the following two conditions: 1) one of the parents is a positive unit which is false in I, or 2) one of the parents and the resolvent are both false in I.

Lemma 1 ([ 4, Theorem 1]). Horn semantic resolution is complete for unsatisfiable Horn sets.

For the rest of this section we use slightly modified definitions of ground clause and ground resolution in order to simplify the analyses of ground deductions .

Definition. A ground clause is a multise t of literals. We use the notation C: -L1 -12 ... - Ln D to represent n occurrences of literal - L in a clause C. D represents the remaining multiset of literals in C.

Definition. Let C1: -L1 ... -Ln D and C2: 11 ... 1m E be two ground clauses where C1 contains at least n occurrences of literal -L and clause C2 contains at least

This work was supported in part by National Science Foundation Grant MCS 79-13252.

SEMANTIC FARAMODULATIO:ili FOR EOR?'-J SETS

William. W. Me Cune LaVJTence J . Henschen

Dept. of Electt"ical Engineering and Computer Science Northwestern Universt ty Evans ton, Illinois , U.S.A.

m occurrences of literal L. D and E a re multi;;ets of literals. The clause C3: D E is a ground resolvent of parent clauses C1 and C2. We say that the set of n oc currences of - L in C1 matches the set of m occurrences of L in C2. Duplicate lite rais in a r esolvent are not merged.

Note tha t a Horn multiset clause still has only one occurrenc e of a positive literal .and that r esolutio!l. of Horn multiset clauses yields a Horn multiset clause.

Lemma 2. Let D1 be a Horn semantic r esolution deduc­ tion of a clause C1 from a ground set S using interpreta­ tion I. Then there exists a Horn semantic resolution deduction D2 of a clause C2 where

1. C2 is logically equivalent to C1, and
2. for each resolution in D2 exactly one literal cf the fal se clause is matched.

Proof. The following algorithm constructs D2 from D 1

1. Choose a highest node in the tree r epr esenting Dl in which more than one lite ral from the false clause is matched. If there is no such node t hen stop; other­ wise, let the parents of the resoluti9n be Pl: -Ll ... -Ln D and P2: L E. The re solvent is R: DE.
2. Replace the above resolution by a sequence of n resolutions. The resolvents are Rl: -Ll ... - Ln- 1 DE, R2 : - Ll ... - Ln-2 DE l E2, ... , Rn: DE l ... En.
3. 3 Resolutions in Dl on descendents of literals in E ar e replaced (recursively) by resolutions on the corresponding multiple copies in El ... En. Go to 1

Neither P l nor P2 can be a positive unit false in I. There­ fore R must be false in I. Because - Lis false in I, each of the clauses R1, ... ,Rn is also false in I. Thus each r esolu­ tion introduced in step 2 is Horn semantic. A highes t node with the given property is selected at each iteration . The deduction is expanded, but only above the select ed node; further, no new node above the selected node has the given property. Thus, the algorithm terminates. Clearly the resulting resolvent is logically equivalent to Cl. QED

Lemma 3. Let D1 be a ground Horn semantic resolution deduction of clause C from ground set S using interpreta­ tion ]. Suppose clause -L EO is false in I and occurs in D1. Suppose also that -L does not occur in C. Then there exists a Horn semantic resolution deduction from S of clause C in which

1. the deduction of - LEO is the same as in D1,
2. -Lis the literal upon which clause - LEO is resolved, and

1. D2 has exactly the same number of nodes as Dl.

Proof. Let the deduction be as shown in Figure la where Ei+ l = (Ei- !MiD u Fi. L and Mi are literals, and Ei, Fi and Gi are multisets of literals. Assume that lit eral - L in clause - LEn descends from literal - Lin clause -LEO. (Recall that duplicate literals are never merged in a resolvent.) Clause - L E l is fal se in I because neither of its parents is a false positive unit. Therefore FO is false. Similarly, each clause - L Ei, and each multiset Fi, CJ:,s;i:Sn, is false in I. Finally, En+ l is false in l. Now con­ sider deduction D2 (Figure 1b) in which the clause L Fn has been moved up in the deduction and resolved with clause -L EO. All other -resolutions remain unchanged. Clearly Gi = Ei-1 + Fn, 1:Si:Sn, is false in I. Thus all resolu­ tions in D2 are Horn semantic. It is clear that D2 has the same number of nodes as Dl. QED

Lemma 4. Similar results to those of Lemma 3 hold for the case in which L EO is the start clause (false in I as before) and En is not empty.

Proof. L Ei , 1:Si:Sn, must be false because its parent L Ei-1 is a false non-unit clause. En+1 is false because En is not empty by hypothesis. The rest of the proof is the same as in Lemma 3. QED

Rema:rk. Lemmas 2 and 3 allow us to assume without loss of generality that given a false clause in a ground Horn semantic resolution dednction, an arbitrary single occurrence of a negative iteral can be chosen as the literal matched for the next resolution.

CoroUary 1. Let S be an unsatisfiable set of clauses, and let I be an interpretation of the symbols of S. Then there exists a resolution refutation of S in which each resolu­ tion satisfies one of the following two conditions:

1. one of the parents is a positive unit false in I. or
2. the parent with the negative literal of resolution and the resolvent are both false in I.

Proof. Let D be a ground Horn semantic r efutation of S which satisfies the conditions of Lemma 2. The following algorithm transforms D into a refutation satisfying the conditions of the corollary.

1. Let C be a highest non-unit clause in D in which the positive literal of the resolution is false in I. If there is no such node then stop.
2. Let - L be a negative literal in C. By Lemma 3 there is a refutation with the same number of nodes in which the deduction of C is the same and -Lis the literal resolved in clause C. Let D be such a refuta­ tion. Go to 1.

At step 1 the deduction of C satisfies the conditions of the corollary. After step 2 the deduction of the child of C satisfies the conditions. Thus the algorithm terminates because D is finite and the transformation does not increase the size of D. QED

Notation. In order to simplify the notation we write Pa for P( ... ,a, ... ) and g(a) for g( .. . ,a, ... ) . Lower case letters a,b,c ,... repres ent terms and upper case C,D,E, .. represent (possibly empty) multisets of literals.

We now consider equality (E-) interpretations and equal­ ity axioms. Note that an E-interpretation will never make the following assignments to ground instances of the equality axioms.

Lemma 5. Let C be a clause with the foll owing properties.

1. C occurs 'in a ground Horn semantic resolution deduction 1Vith respect to E- interpretation J.
2. C contains a positive literal L that is true in I, L des­ cends from an equality axiom, and any remaining literals of C are false in J.

Then C also has one of the following properties.

1. C is itself th '3 equality axiom.
2. C is a unit clause obtained by resolving two false positive units with either transitivity <ttt> or predi­ cate substitution <ttt>.
3. C is an immediate resolvent of function substitution <tt> with a false positive unit.
4. C is an immediate resolvent of predicate substitution <tft> with a false positive equality unit.

Proof. Trivial by case analysis.

Lemma 6. Let C be a clause with properties 1 and 2 above but with .L a negative equality literal, a,.. b.

Then C also has one of the following properties.

1. C is itself the equality axiom.
2. C is an immediate resolvent of predicate substitution <ttf> with a false positive non-equality unit.
3. C is an immediate resolvent of transitivi ty <ttf> with a false positive equality unit.

Proof. Trivial by case analysis .

Theorem 1. Let S be an E-unsatistiabl2 se t of ground Horn clauses, and let I be an E-intenJr-e: c:.tion for the symbols of S. Then there exists a resohi:icn and paramo­ dulation refutation of S u !a=ai a is c. 6!'"0U.'"ld terr:1l in which each resolution is Horn semantic ar:d each paramo­ dulation satisfies one of the following two conditions:

1. both parents are pos itive units which ar e false in I. or
2. one parent and the paramodulant ar e both false in I.

(Paramodulation is defined so that either the left or r ight argument of an equality literal can match the term to be replaced.)

Remark. We assume symmetric matching for equality. That is, we allow the literals a=b and b,.<a to match for a resolution. This simplifies the proof of the theorem and does not weaken the theorem.

Proof. There exists a finite set E' of ground instances of equality axioms such that S u E' is U.'"lsatisfiable. We know from Lemma 1 that there exists a r esolution r efuta­ tion, say D1, which satisfies the re solution r estr ictions of the theorem. We will construct from D1 an acceptable resolution and paramodulation refutation D2.

Because we are assuming symmetric matching for equal­ ity and paramodulatir .1 is allowed from both sides of the equality, we may assu,ne without loss of generality that D1 contains no instances of symmetry.

Let the initial deduction D1 be written as a tree with the false parent of each node on the left. We transform Dl by repeatedly replacing the leftmost occurrence of an equal­ ity axiom by paramodulation. Because the equality axiom is true , it must occur as the right parent where it enters Dl. Because equality axioms are eliminated left to right , no literal to the left of the axiom being eliminated can descend from another equality axiom. Special cases (A.l, A.2) are introduced to handle the replacement when an earlier replacement has caused p aramodulation into or from a descendant of an equality axiom occurring further to the right. Each of the cases below is labeled with the type of equality axiom (P for predicate substitu­ tion, T for transitivity, etc) as well as with the truth value assignments for its literals. Due to space limitations, we describe in prose only a few of the cases. The remaining ones are similar and are described by the Figures 2-20.

Case P.ttt (Figure 2) . The two negative literals must resolve immediately with fa lse positive units a=b and Pa. The order is not important. The resulting paramodu­ lation introduces no new cases because both parents of paramodulation were to the left of P.ttt.

Case P .tfl' (Figure 3). The true literal a,.<b must r esclve first. Lemma 3 allows us to assume that -Pa r esolves next . The resolution is replaced by a paramodulation as shown in Figure 3. If Pa descends from another equality axiom, that axiom is eliminated by special case A.l.

Case P .ftf (Figure 4). The true literal - Pa must resolve first. Lemma 3 allows us to assume that a,.<b resolves next. If a=b descends from another equality axiom, that axiom is eliminated by special case A.2.

Case A.l. Paramodulation into a true positive non­ equality literal that descends from an equality axiom. Let the clause be Pb C, where Pb is true and C is false. By Lemma 5 there are possible 4 subcases.

Subcase A. 1.1 (Figure 16). Pb C is predicate substitution with paramodulation into Pb. Lemma 3 allows us to assume that the two negative literals resolve next. The order is not important. This section of the deduction is replaced by two paramodulation i:llerences. Paramodula­ tion from a=b is covered in case A.2, and paramodula­ tion into Pa is covered in case A. 1.

The remaining 17 cases are similar.

QED

Theorem 2. Let S be an E-unsatisfiable set of (general) Horn clauses and let I be an E-interpretation for the sym­ bols of S. Then there is a resolution and paramodulation refutation of S u lx=xl u !functional reftex1ve axiomsj satisfying the semantic conditions of T'neorem 1.

Proof. Let D' be a proof as in Theorem 1 for an appropri­ ate set S' of ground instances of S. Resolutions in D' are lifted in the normal way. Now let T'[b'] be the grour..d paramodulant of T'[a'] and a'=b' C', and let T and a=b C be the corresponding clauses of S. If the position in T corresponding to the position of a' in T'[a'] exists, then paramodulation lifts directly. If not, functional reflexive axioms are used.

Case 1. T'[a'] is false. The appropriate set of functional reflexive axioms are paramodulated into T to instantiate it so that it gets a sub term corresponding to a'. Each paramodulant is false because each has T'[a'] as an instance. The paramodulation now lifts directly.

Case 2. T'[a'] is true and a'=b' C' is false. In this case, a=b C is paramodulated into the appropriate functional reflexive axioms to obtain a clause g( ... (a) ... )=g( ... (b) ... ) C which can match the existing term structure in T'[a']. g( ... (a) ... )=g( ... (b) ... ) is false because T'[a'] is true and T'[b'] is false. Thus each paramodulant is false. The paramodulation now lifts directly. QED

In case F.tf (Figure 14) of Theorem 1, paramodula­ tion is into a subterm of an instance of x=x. All other uses of instances of x=x are for resolution. We believe this type of paramodulation can be avoided by making the transformation as shown in Figure 21. Lemma 4 allows us to assume that the equality is the next literal to resolve in clause C g(a)=g(b). Now the newly introduced paramodulation is into a level 2 subterm of a true nega­ tive equality which may descend from ·another equality axiom. This introduces a host of new cases; further, this case is recursive -- we must handle the case in which an arbitrary subterm of a descendant of an equality axiom is paramodulated. All of these cases have not yet been analyzed.

Of course, functional reflexive axioms cannot be eliminated entirely under the present semantic restric­ tions. Consider the clauses 1. -P(x,x), 2. P(f(a),f(b)), and 3. a= b. We may chose an interpretation in which the first clause is false and the other two are true. Then the only semantic refutations possible require paramodula­ tion from a functional reflexive axiom. It has been shown in practice [ 17] that inclusion of the functional reflJ xive axioms severely degrades the performance of the pro­ gram. Some strategies for paramodulation are complete without them [1,5], and we conjecture that there is some modified version of semantic paramodulation for Horn sets that is complete without these axioms.

3. P.elated Results

T. Brown and Li da Fa have reported independently on similar research. Brown [2] proves the completeness of a version of semantic resolution and paramodulation for Horn sets. His conditions on resolution are the same as ours, but his conditions on paramodulati::m are weaker. There is a restriction only on the into parent -- it must either be a false positive unit or have the equality true and the remaining literals false. (Brovm defines paramodulation differently so that all occurrences of a term in the into clause are replaced.) His method of proof is induction using the excess literal parameter introduced by Bledsoe. Li da Fa [6] has reported a com­ pleteness proof with conditions similar to ours but he assumes a very limited class of Herbrand interpretations -namely those in which two terms are equal if and only if they are the same sequence of symbols. His proof is immediate. We are not aware of any reports of experi­ mental results with either of these methods.

4. Experimentation

We plan to conduct extensive experimentation with semantic paramodulation using NUTS (Northwestern University Theon,m-proving System) [ 1 0]. an L:;IA-based theorem prover [7,8]. Of course, we will use various tech­ niques for efficient evaluation of clauses [e.g .. 4] and methods for insuring that later substitutions in the deduction don't eliminate all fal se instances of an earlier false parent [ 11,12].

While it wi.ll be interesting enough to compare Horn semantic paramodulation with other paramodulation strategies, the main emphasis in our experiments vrill be to determine, if possible, what kinds of interpretations lead to good performance. Experience has shown [ 4,12] that for resolution, choosing the wrong interpretation leads to little or no improvement over simple set-of­ support resolution. This is also true for paramodulation . For example , if we have all unit equalities (very often the case) and the interpretation assigns only the negative clause to be false, then the only allowable semantic paramodulations are those from any of the (true) positive equality units into the one false negative unit. Moreover, the resulting negative unit also will be fal se. Such an interpretation allows exactly the same paramodulations as if we had chosen the one negative clause to be the set of support. On the other hand, if we choose an interpre­ tation in which the negative clause is true, but some spe­ cial hypotheses are false, then the only initial paramodu­ lations allowed are paramodulations from or into the false equality units which result in false paramodulants or between pairs of these false special hypotheses. If we have chosen a good interpretation. there will be fewer of these than one would get by allowing those special hypotheses to be in a set of support.