Completeness Theorems for Semantic Resolution in Consequence-Finding

1. Introduction

The consequence-finding problem which has been described by Lee [i) may have the following form: Given statements A 1 , ··· , An, find a statement B such that B follows from A , ··· ,A. It may well 1 n be that A, ··· ,A 1 n are the axioms or postulates of some theory, and B is a new logical consequence of that theory possible not found before. A proof­ finding problem is a problem which is given a theorem and asked to find a proof for the theorem [6]. In this paper, we shall restrict ourselves to first-order predicate calculus, and consider only the cases where A , ··· ,A and Bare 1 n (quantifier-free) clauses [i,4,5,6]. Clearly, under this formulation, if B is the empty clause, consequence-finding reduces to proof-finding. Hence, consequence-finding may be considered more general than proof-finding.

Because of the relation between consequence­ finding and proof-finding, most of the strategies [3-7,9,1Q] used in proof-finding can also be used in consequence-finding. In [2] Lee proved that Robinson's ordinary resolution principle [4], which is for proof-finding is also complete for consequence-finding. The .present paper will extend the semantic resolution of Slagle (7] to consequence-finding, and prove that given an interpretation I, any prime consequence B, which is false in I, can be derived from a set of axioms (or postulates) A , ··· ,A by applying !-(semantic)

1 n

resolution. In order to be more in keeping with standard practice, we use "interpretation" rather than "model," which was used in [7]. Our theorems are more general than Lee's results. The defini­ tions, theorems, and proofs in this paper follow closely those given in [7]. It is also assumed that the reader is familiar with Robinson's review article [6] ·

2. Prime· (Non-trivial) Consequences

In this section, we shall define a prirre consequence, and use this concept to explain completeness theorems in consequence-finding.

J.R. Slagle, C.L. Chang, R.C.T. Lee National Institutes of Health

Bethesda, Maryland

Roughly speaking, we shall prove below completeness theorems which show that ordinary resolution will generate all the prime consequences of a set of clauses and that semantic resolution will generate all the prime consequences which are false in the interpretation used in the semantic deduction. It is possible that both kinds of resolutions may or may not generate some non-prime consequences.

Definition. An interpretation of a set S of clauses consists of a nonempty set U called a universe (sometimes, to emphasize the universe U, we say an interpretation over U.) and an assignment of "values" as follows to each individual symbol, function symbol and predicate symbol occurring in S: (i) to each individual symbol, we assign an element in U; (ii) to each function symbol with n arguments, we assign a function whose n variables range over U and whose values are in U; (iii) to each predicate symbol with n arguments, we assign a function whose n variables range over U and whose values are the truth values, true and false. When S is a set of ground (variable-free) clauses, we call an interpretation of S a ground interpretation.

Definition. A ground instance of a clause C over a universe U is a ground clause obtained by sub­ stituting elements of U for all the variables in c.

We note that if U is the Herbrand universe H of S, then an interpretation of S over H may be represented by a sequence m 1 , m , ··· , m., ··· in 2 J which mj is either Aj or ,..,A j, where A 1 , A 2 , ··· , Aj, ··· are the distinct ground instances of atoms of S over H.

Definition. An interpretation I of a set S of clauses over a universe U is said to satisfy a clause C in S (or C is true in I) iff every ground instance of C over U is~e in I. Otherwise, I is said to falsify C (or C is~ in I).

Definition. A set S of clauses is said to be satisfiable iff there is an interpretation I of S such that I satisfies all the clauses in s. Other­ wise, S is said to be unsatisfiable.

Definition. A clause C is said to be a logical consequence of a setS of clauses c 1 , ··· , Cq' (or C follows from c 1 , ··· , Cq), iff for every interpretation I of (S & C) if I satisfies c 1 , ··· , C , I also satisfies C. When no confusion is q possible, we shall sometimes say that C is a logical consequence of c 1 , ··· , Cq. We note that if C is a logical consequence of S, every instance of C is also a l ogical consequence of s.

It is noted t hat if a clause B is a l ogical consequence of a clause A, and if B and A have the corresponding well - formed formulas B'' and A' respec­ tively, then g is a l ogical consequence of A', but not conversely. For example, let A' =gx"yPxy and g = Vy 3 xPxy. The corresponding r espective clauses of A' and g are A = Pay and B = Pf(y)y, Clearly, g i s a logical consequence of A', but B is not a l ogical consequence of A.

We now prove a generalization of Herbrand's theorem.

Theorem 1. A ground clause C is a logical con­ sequence of a set S of clauses iff there is a finite set ~ of ground instances of clauses in S over the Herbrand universe of (S & C) such that C is a logical consequence of ~.

Proof, C is a logical consequence of s.

• ~Every interpretation which satisfies S must satisfy c.
• {:=:;>Every interpretation must falsify (S &-C), where .-c is the negation of C,
• ¢;::;> (S & ..... c) is unsatisfiable,
• ~By the Herbrand theorem, there is a finite set S' of ground instances of clauses in S over the Herbrand universe of (S & C) such that (S 1 &.-G) is unsatisfiable.
• ~ Every interpretation which satisfies S must falsify'""C (or satisfy C),
• ~ C is a logical consequence .of ~,

We note that Theorem 1 cannot· be further generalized to the case where C is a clause. A counterexample is that S = {P(x)jand C = P(f(x)),

Definition, Let S be a set of clauses. A clause C is said to be a prime* (non-trivial) consequence of S iff C is a logical consequence of S and there exists no other logical consequence D of S such that C is a logical consequence of D. A logical consequence of S is a non-prime (trivial) conse­ quence of S iff it is not a prime consequence of s.

We note that if a set S of clauses is unsatis­ fiable, the empty clause is the only prime conse­ quence of S.

Definition. If C and D are two clauses, we say that C subsumes D iff there is a substitution ~ such that C~ S. D. Clearly, if a ground clause C subsumes a ground clause D, then C ~D.

We note that if C subsumes D, D is a logical consequence of c. We also note that there is a procedure which can decide whether or not a clause C subsumes a clause D.

* We note that a prime consequence of a set of gr ound clauses is a prime implicate of the set and is the dual of a prime implicant of the dual of the set [a].

3, Completeness Theorem for Propositional Calculus

We now state and prove our basic resul ts in Theorem 2 and 3, Theorem 2 and 3 of the present paper are the respective extensions of Theorem 5 and 6 of Slagle's paper [7].

Theorem 2, If a ground clause C is a l ogical consequence of a finite set S of gr ound clauses but is not subsumed by any one clause in S and if C contains no negative literals after a renaming r and if the first atoms in an orde ring A of the atoms in S & C are the atoms inC, then there

exists an unresolved maximal Ar-clash [ El' E 2 , · ·· , E , N_{ inS with nucleus N such that any set q consisting of N and one or more of the e lectrons

E 1 , E 2 , ··· , Eq is an unresolved Ar-clash inS.

Proof. The following proof follows closely that of Slagle [7].

Let R be the renamable subset corresponding to the renaming r. Because of renaming, we can with­ out loss in generality assume that R is the posi­ tive subset of S, that C is a positive ground clause, and that r is the empty renaming. Let A be the sequence Al, A2, .. -., Ak. The literals in C are the first p atoms in A, Let Ip be the

sequence ,.Al, ··· , ,.,.,AP. We note that no R-clause consists entirely of complements of literals in Ip because noS-clause subsumes C. For j = p + 1, ··· , k, form the sequence Ij as follows:

I.= ,] if some R-clause consists of complements of literals in the sequence I .....,.Aj · j-1, , I. 1 ,~Aj if noR-clause consists ]- entirely of complements -of literal s in the sequence I . , ,....Aj J-1

Let I be Ik. From the construction, it i s obvious that the ground interpretation I satisfies (R & ~c). In addition it is clear that, for every positive literal Ai whi~h appears in I, there is an R-clause Fi such that AL is the largest atom in Fi and such

that a,ll Fi ·.li.terals other tha~ Ai are false in I. Since C is a logical consequence of S, (S &~C) is truth-functionally unsatisfiable. Since I satisfies (R &"'C), I must falsify one or more clauses in S - R. Of all the S-clauses which I falsifies, let N be one of those which contains the fewest negative literals. Let-B 1 , ~ 2 , ··· , ~Bq be all the negative literals in N. Let

i = 1,2, ··· ,q. For each i, Bi is true in I. Hence for each Bi, there is an R-clause Ei such that Bi is the largest atom in Ki and such that all Ei - literals other than Bi are false under I. (Note that for each i, Bi = Aj for some j; hence we can let Ei be Fj,) Hence no literal in Ei -

[ BiJ is Bj for j i i (since such Bj are true in I) nor is it the complement of any literal in N-~~B 1 , """B2, ... ,....,Bq ] (since such literals are false in I). It follows that any set whose members are N and one or more of the clauses E 1 , E 2 , ··· , Eq is an Ar-clash in S whose resolvent is false under I and contains fewer negative literals than does N. Therefore the resolvent of any such clash is not in S and so the clash is unresolved in s. The proof is now completed by noting that the clash [El, E2, ... , Eq, N} is maximal.

By Theorem 4 of Slagle [7], the following theorem is also true,

Theorem 3, If a ground clause C is a logical consequence of a finite set S of ground clauses but is not subsumed by any one clause in S and if C is false in a ground interpretation I of (S & C) and if the first atoms in an ordering A of the atoms in S & C are the atoms inC, then there exists an unresolved maximal AI-clash ["E 1 , E 2 , ··· , E , N} inS with nucleus N such that any set q consisting of N and one or more of the electrons E 1 , E 2 , ··· , Eq is an unresolved AI-clash ins.

Although the theory can now be extended to semantic and renamable resolution, we restrict ourselves to semantic resolution in the remainder of tliis paper,

Theorem 4, If a ground clause C is a logical consequence of a finite set S of ground clauses and is false in a ground interpretation I of (S & C), and if the first atoms in an ordering A of the atoms in S & C are the atoms inC, then there is a ground maximal AI-deduction from S of some ground clause T which subsumes C.

Proof. Let S be S. In general, for j ~ o, if there is no g~ound clause T in Sj which subsumes C, let Sj+l be the result of adding to Sj the ground maximal AI-resolvent obtained as in Theorem 3, This gives a nested sequence S 0 , s 1 , ··· , of sets of ground clauses. The sequence cannot con­ tinue to grow since the successive resolvents are all constructed from the same fixed finite set of literals, namely, those which occur in members of S. Hence there are only finitely many such re­ solvents which can be added. Therefore, for some j ~ o we have a ground clause T in S such that C is subsumed by T. Tracing the an~estry of T from S then gives the required deduction,

There .is a difficulty in applying Theorem 4 to deduce logical consequences from S because C is generally unknown beforehand and we cannot have an interpretation of (S & C). However, if we consider prime consequences of S, this diffi­ culty can be easily overcome, To see this, let C be a prime consequence of S in Theorem 4. Thus, T = C, i.e,, C can be derieved from S, Hence, every symbol which occurs in C occurs in S. In this case every ground interpretation of S is a ground interpretation of (S & C), and vice versa. Therefore, we have the following completeness theorem which follows from Theorem 4, Theorem s. If a ground clause C is a prime con­ sequence of a finite set S of ground clauses and is false in a ground interpretation I of S, and if the first atoms in an ordering A of the atoms in S are atoms inC, then there is a ground maximal AI-deduction of C from S.

We note that if a finite set S of ground clauses is unsatisfiable, the empty clause 0 is the only prime consequence of S. Since o is false in every interpretation, Theorem 5 reduces to a theorem from which the previous completeness theorems given in ~-7, 9, 10~ for resolution (including ordinary, hyper-, and set~of-support resolution) in proof-finding can be derived [7].

4. Completeness Theorem for First-order Predicate Calculus

The above theorems in Section 3 hold for propositional calculus. We now extend them to first-order predicate calculus.

Theorem 6, If a clause C is a logical-consequence of a finite set S of clauses and is false in an interpretation I of (S & C), then there is an !-(semantic) deduction from S of some clause T which subsumes c.

Proof, Let x 1 , ··· , xm be the variables occurring in C. To concentrate on the variables in C, we shall represent Cas C(x 1 , ··· ,xm)' Let U be the universe over which I is defined. Since C(x 1 , ··· ,xm) is false in I, there are elements a 1 , ··· , ~in U such that the ground instance C(a 1 , ··· ,~) of Cis false in I. Let b 1 , ··· ,bm be new distinct individual symbols not occurring in (S & C) and let H(b 1 , ··· ,bm) be the Herbrand universe of [s & C(bl,····bm)], We define an interpretation IH of (S & C) over H(b 1 , ··· ,bm) as follows: A ground literal Lover H(b 1 , ··· ,bm) is in IH iff the ground literal obtained from L by substituting ai for bi' fori= l, ··· ,m, is true in I. (We note that the definition for IH is self -consisten~

Clearly, by this definition, C(b 1 , ··· ,bm) is false in IH. Since C(x 1 , ··· ,xm) is a logical consequence of S, C(bl·····bm) is a logical consequence o[ s. By Theorem 1, there is a finite set ~of ground instances of clauses inS over H(b 1 , ··· ,bm) such that C(b 1 , ··· ,bm) is a logical consequence of S'. Let I~ be the ground interpretation of [s' & C(b 1 , ··· ,bm)J corresponding to the interpret ation IH. Since C(b 1 , ··· ,bm) is a log ical consequence of S ' and is false in Ili and there exists an ordering A as required by Theorem 4, by Theorem 4 there is a ground maximal AIR-deduction from S' of some ground clause T'which subsumes C(b 1 , ··· ,bm). For this deduction tree Tr, we attach to each node of Tr a further clause over and above the clause a lready there as follows: To each initial node of Tr, attach the corresponding S-clause of which the clause already there is an instance. Then for each non-initial node of Tr, if clauses have been attached in this way to each of its immediate predecessor nodes and constitute the set W, attach to it that I -resolvent of the latent IH-clash W H of which the clause already there is an instance. In this f ashion, a clause is attached to each node of which the clause already at the node is an in­ stance . Let the clause attached to the terminal node be T. Since each IH-clash is an !-clash, the deduction of T is an !-deduction. Since T does not contain the individual symbols b 1 , ··· ,bm for T is derived from S, and T' .. which subsumes C(b 1 , ··· ,b) is an instance ofT, there must exist a m substitution O"(b 1 , ... ,bm) such that TcY(b 1 , ··· , bm) = T'~C(b 1 , ... ,bm)· So that, To-(x 1 , ... ,xm) :c<x 1 , ··· ,xm)' i.e. T subsumes C. This completes our proof.

As in ground case, in Theorem 6, if C is a prime consequence of S, then T = C. Since C can be derived from S, every symbol which occurs in C must occur in s. Therefore, we can use interpre­ tations of S, instead of interpretations of (S & C), in the following completeness theorem for first­ order predicate calculus.

Theorem 7. If a clause C is a prime consequence of a finite set S of clauses, and is false in an interpretation I of S, then there is an !-(seman­ tic) deduction of C from S.

The following theorem follows directly from Theorem 7:

Theorem 8, If a clause C is a prime consequence of a finite set S of clauses and contains no negative (positive) literals, then there is a positive (nega tive) hyper-deduction of C from S.

We now consider the theorems for unit clauses because prime consequences which are unit clauses are interesting. In this case, we can use PI­ deduction instead of !-deduction as stated in the following.

Theorem 9. If a unit clause C is a prime conse­ quence of a finite set S of clauses and is false in an interpretation I of S and if the first predicate symbol in an ordering P of the predicate symbols occurring in S is the predicate symbol in D, then there is a PI-deduction of C from s.

The proof is the same as the proof for Theorem 6 except we carry the ordering of the predicate symbols from the ground case to the latent case.

The following theorem is a corollary of Theorem 9:

Theorem 10. If a positive (negative) unit clause C is a prime consequence of a finite set S of clauses and if the first predicate symbol in an ordering P of the predic ate symbols in S is the predicate symbol inC, then there is a positive (negative) P-hyper-deduction of C from S.

We now give an example to illustrate our results.

Example, left and there is In an associative system, if there right solutions, then we can derive a right identity. are that

The system is expressed in three clauses:

Al: .....,.p(x,y,u) V-P(y,z,v) V.-P(x,v,w) V P(u,z,w) part of associativity

A2: P(g(x,y),x,y)

A3: P(x,h(x ,y),y)

Bxistence of a left solution

Existence of a right solution

Since we know beforehand that the theorem concerning the right identity is a positive unit, we use a negative interpretation to guide our deduction. The electrons in the deduction will be positive clauses and the deduction uses positive hyper-resolution.

R3 means that there is a right identity.

s. Conclusion

In the preceding sections, we have given several completeness theorems for consequence­ finding. Using !-(semantic) resolution, from a finite set of axioms, we can generate at least the prime consequences which are false in I. Semantic resolution reduces the number of clauses we have to generate in order to derive these prime con­ sequences.

In consequence-finding, it is difficult to find a criterion for interesting consequences. In this paper, we have given the definition of a prime consequence. We believe that many interesting con­ sequences may be obtained from prime consequences. However, much work needs to be done in this area.

In addition to generating interesting conse­ quences, consequence-finding may also be relevant to proof-finding. The theoretical framework given ffire reveals part of the behavior of semantic re­ solution. It shows that semantic resolution gener ates prime consequences of any subset of a set of clauses. This gives us more insight into semantic resolution and may prove to be useful in proof-finding. For example, in proof-finding, we are interested in deducing a pair of contradictory units. From Theorem 10, these contradictory units can be deduced by using positive and negative P-hyper-resolution simultaneously. We may call the str ategy that uses positive and negative P­ hyper-resolution simultaneously the "bridging strategy." In most cases, positive hyper-resolu­ tion corresponds to thinking forward from axioms whereas negative hyper-resolution corresponds to thinking backward from conclusion. This is a good sign because people reason in both directions when proving difficult theorems. Therefore, a program that implements the bridging strategy corresponds to a theorem prover who thinks forward and back­ ward simultaneously. The bridging strategy may be useful for theorems which require long proofs. Since unit clauses are either positive or negative the unit section of the unit preference strategy, which is the most efficient strategy ever im­ plemented on computers, is a special case of the bridging strategy.