Subsumption And Connection Graphs

1. INTRODUCTION

R. Kowalski's connection graph proof proce­ dure [K75] represents a set of logical for­ mulae not as a set but as a graph like structure. Inference rules such as resolu­ tion and factoring are expressed as opera­ tions on that graph. In addition to these operations, which usually expand the graph, the procedure also provides for deletion operations that remove certain components from the graph. Other approaches based on graphs have been proposed by [SI76],[SH76],

[ AN 79 ] , [ B 7 9 ] .

One of the striking properties of the connection graph proof procedure is that application of a deletion operation can result in the applicability of further de­ letion operations, thus potentially leading to a snowball effect which rapidly reduces the graph. The probability of this effect r ises with the number of deletion rules available.

A very powerful deletion rule for resolu­ tion based systems is the subsumption rule ([L7BJ, chapter 4). Unfortunately a test

SuBSUMPTION AND CoNNECTION GRAPHS

Norbert Eisinger

Institut fUr Informatik I Universitat Karlsruhe D-7500 Karlsruhe 1, Postfach 6380

for subsumption is very expensive and is usually implemented only for restricted cases. In this paper a test for subsumption based on the principal idea of the connec­ tion graph proof procedure is developed, which in contrast to the standard test ([L7BJ) is sufficiently efficient to permit unrestricted subsumption in practical cases. Though not limited to it, the test is most naturally embedded into the connection graph proof procedure, but unrestricted combina­ tion of subsumption, tautology, and purity deletion is shown to render the connection graph proof procedure inconsistent.

2. DEFINITION AND NOTATIONS

The paper is based on the first order pre­ dicate calculus with the usual notational conventions for constants, variables, terms, atoms, literals, and clauses. The number of literals in a clause Cis denoted by lei. The empty clause is denoted by o. The ele­ ments in a set of clauses are always assu­ med to be variable disjoint.

A substitution is a mapping cr from varial::!es to terms identical almost everywhere. It is extended to mappings on terms, atoms, li­ terals, and clauses by the usual homomor­ phism. A unifier for two terms (or literals) s, t is a substitution cr for which cr(s) = cr(t). If for any other unifier 0 for s, t there is a 0' with 0 = 0'ocr, we say cr is a most general unifier (mgu) for s and t. Two li­ terals are called a-complementary, if they are of opposite sign and cr is an mgu for their atoms. Two substitutions a, 0 are strongly compatible, if for each variable v: a(v)*v A 0(v)*V · a(v)=0(v). Note that for a set of pairwise strongly compatible substitutions their functional composition is commutative.

• A connection graph is a pair (C, L) for .,.,·hich
• C is a set of clauses
• Let LIT = ~c be the set of all lite­ rals occuring in the clauses of C. Then L c C x LIT x C x LIT is a relation such that
• (C,L,C' ,L' )EL .. C * C', LEC, L'EC', L and L' are a-complementary
• (C,L,C',L')EL · (C',L',C,L)EL

The graph is said to be total, if condition 2a) also holds in the opposite direction. A literal L in a clause C is pure, if there are no C', L' such that (C,L,C',L')EL. The elements of L are called links. They con­ nect a-complementary literals in different clauses, thus indicating possible resolu­ tions.

The connection graph proof procedure defined in [K75] processes a set C of clauses in the following way: first all possible links within C are computed, i.e. a total graph (C,L) is constructed. This graph is then reduced by some deletion rules yielding another total graph. Next a link is selec­ ted and its resolvent created and incorpo­ rated into the graph together with all its factors. Then the link resolved upon is de­ leted from the graph and again the reduction rules are applied. The next link is selected

and so on until oEC or L = ¢.

Incorporating a new clause into the graph means creating all links between its lite­ rals and the rest of the graph. A literal in a resolvent or factor has to be connected to all those places in the graph to which at least one of its parent literals is connec­ ted by a link. Thus the links are simply in­ herited. In addition to these inherited links all links between a resolvent (or factor) and its parent clauses have to be ex­ plicitly computed, or, more efficiently, derived from "autolinks" between comple­ mentary literals in self resolving clauses ([B75]).

The reduction rules contribute both to the practical attractivity and the theoretical difficulties of the connection graph proof procedure. The original rules are: delete a clause if it contains a pure literal run delete a clause which is a tautology. Fur­ ther possible rules include: delete a link if its resolvent is a tautology [WA81], delete a clause if it is subsumed by an­ other clause in the graph, delete a link if its resolvent is subsumed by another clause in the graph. Note that each dele­ tion may cause a purity to arise, thereby causing further deletions. It is not yet known as to which combinations of these deletion rules preserve the completeness of the procedure.

3. SUBSUMPTION AND THE S-LINK TEST

Let C and D be clauses. C a-subsumes D, if ICI $ IDI and a is a substitution such that a(C) :. D. Throughout this paper the terms subsumption and a-subsumption will be used interchangeably, though usually subsumption is defined more generally than a-subsurnption (see [L78J).

The standard test for a-subsumption works as follows: given C and D, first make sure that ICI $ IDI and that Dis not a tauto­ logy. Then negate D and change variables in D to constants, yielding a set n of ground unit clauses. c a subsumes D iff o is derivable from {C} u D. (Details can be found in [Cl73] and [L78].)

The positive aspect of this subsumption test is that it uses the same mechanism which underlies the entire deduction sy­ stem, i.e. resolution. But from a practical point of view this turns out to be a dis­ avantage. Normally one has to check for subsumption as soon as a new clause is ge­ nerated, i.e. after each resolution step. This means that each "major" resolution step is followed by several "minor" resolution steps for the subsumption test, thus multi­ plying the overall expense. Yet even worse, given a resolvent C there is no hint as to which clauses pot_entially subsume or are subsumed by C. So the test, already expen­ sive in itself, has to be performed within an iteration over all elements of the given set of clauses. In practice, of course, one would first make sure that the predicates are in common, so that the test is not per­ formed during each iteration step.

The resulting cost is such that for practi­ cal systems only restricted versions of stib­ sumption are implemented, e.g. only for cases where the subsuming clause is a unit. Omitting subsumption, on the other hand, can cause considerable redundancies.

The central problem for a subsumption test consists in efficiently finding out which literals in which clauses are unifiable. Disregarding the signs of the literals this corresponds to the very same problem that arises when two clauses have to be selected for the next resolution step. In both cases comparing all literals of all clauses is a possible but inefficient solution.

In the resolution case the connection graph procedure provides for a more efficient alternative. The literals of a set of c lauses are compared with each other once and forever when the initial graph is con­ structed. Subsequently the necessary infor­ mation is directly available in the form of the links. Because of the inheritance mechanism for links the new literals in resolvents and factors need not go through any search process either. Thus the problem of finding two resolvable clauses is reduced to simply picking a link.

This basic idea can be applied to the sub­ sumption problem by introducing links of a new type that connect unifiable literals. Formally we define a subsumption graph (S­ graph) as a pair (C, S ) such that

1. C is a set of clauses
2. Let LIT = tJc be the set of all literals occuring in the clauses of C. Then ;; c (" ' LIT ' C x LIT is a relation such that
3. (C,L,C',L')ES .. C * C', LEC, L'EC', L and L' are unifiable
4. {C,L,C',L')ES · (C',L',C,L)ES

The S-graph is said to be S-tatal, if condition 2a) also holds in the opposite direction. A literal L in a clause C is s­ pure, if there are no C', L' such that {C,L,C' ,L')ES . The elements of S are called S-links.

Given a set of clauses to be refuted, we initially compute all possible S-links between literals in these clauses. When a new resolvent or factor is derived, the s­ links are inherited from the parent clauses in the same way as are the resolution links in the connection graph proof procedure. But in contrast to resolution links {R­ links) S-links are never deleted, unless one of the parent clauses is removed from C. It can be shown easily that under. these circumstances the S-graph remains s-total throughout the entire computation (see [EBO)).

In order to develop a subsumption test using S-graphs we need some further de­ finitions:

Let (C, S ) be an S-graph, CEC a clause and LEC a literal.

We define con(C,L) := {DEC I 3KED(C,L,D,K)ES} as the set of all clauses connected to L in C by S-links.

Further let sub(C) := ~con(C,L) be the set of all clauses connected to every literal in L by S-links.

For LEC and another clause DEC we define uni(C,L,D) := {cri3KED{C,L,D,K)ES" cr(L) =K} as the set of all matching substitutions mapping L onto some literal in D. Finally let u 1 , ... ,un be sets of substitutions. Then merge (u 1 , ... ,Un) :={(a 1 , ... ,an)Eu 1 x ... xunlthe ai are pairwise strongly compatible} is the subset of their cartesian product, for which the functional composition of the components yields a unique substitution regardless of their order.

The subsumption test is provided by the following theorems:

Theorem 1

Let (C,S) be an S-total subsumption graph and c = {L 1 , ... ,Ln}ES a clause, n ~ l. Then for DEC

c a-subsumes D iff ICI s IDI A DEsub(C) A merge(uni(C,L 1 ,D), ... , .uni(C,Ln,D)) * ¢.

Theorem 2

Let (C,S) be an S-total subsumption graph and D = {K 1 , ... ,Km}EC a clause, m~ l. Then for c * o

n c a-subsumes D only if cEbj 1 con(D,Ki). Detailed proofs can be found in [E80].

The following example illustrates the prin­ ciple of a test based on Theorem 1. Assume the set of clauses C = {c,D 1 ,D 2 ,D 3 ,D 4 } with c = {Pub,Quv}, D 1 = {Pxy,Qya}, D 2 = {Pzb,Pab,Qab}, D 3 = {Pww,Pw}, D 4 = {Qaa,Rb}. We want to find all clauses subsumed by C. In this case only S-links connected to C are relevant, so for reasons of clarity all other S-links are omitted in the S-graph for C:

Now ICI s IDil for all i and sub(C) = {D 1 ,D 2 }, because D 3 and D 4 are each oonnected to only one literal of C. We have to asso­ ciate with each literal of C a set of matching substitutions for each clause in sub(C). In this case uni(C,Pub,D 1 ) =¢be­ cause there is no a such that a(Pub) = Pxy. Thus D 1 can be disregarded.

For D 2 we obtain uni(C,Pub,D 2 ) {u := z},

{u := a}}and uni(C,Quv,D 2 l ={{u:=a, v:=b}}. The substitutions {u := a} and {u := a, v := b} are strongly compatible, thus C subsumes D 2 (but none of D 1 ,D 3 ,D 4 l.

The main point of the test is that the ex­ pensive unification is postponed until the function sub preselected a plausible sub­ set of candidates for subsumption. In case we are looking for subsuming rather than subsumed clauses, this preselection process is slightly more complicated. By Theorem 2 we first determine all clauses connected by at least one S-link to the given clause D. Then from this set we ascertain those C for which ICI s IDI and DEsub(C) holds and only then the unification operations are performed.

In both cases this preselection and the fact that the literals to be unified are explicitly known, can save considerable time. On the other hand some effort has to be invested for the computation of all s­ links in the initial graph. As with the connection graph proof procedure this ad­ vance cost can be higher than a possible gain, if the set of clauses is only small. For more complex examples however, there is certainly a pay off. But of course any gain in time has to be paid for by additio­ nal storage needed for the S-links.

4. REFINEMENTS OF THE S-LINK TEST

The inheriting mechanism for S-links can be optimized in the same way as described in [B75] for resolution links. Here the proofs are very simple because S-graphs are always total.

Another refinement results from the obser­ vation that for a clause C containing an S-pure literal sub(C) = ¢. That means that such a clause cannot subsume any other clause.

When computing the uni(C,Li,D) we need to know which KED are unifiable with Li. As the definition of uni shows, these are exactly those literals we already had to consider for the computation of con and sub. The information obtained during the compu­ tation of con and sub should be stored in an appropriate data structure to avoid having to recompute it for uni.

Thus far the S-link test was developed with­ out considering the underlying inference mechanism. Since they are based on the ~ principal idea as connection graphs, s­ graphs appear to be combined most naturally with this inference method. We can modify the definition of a connection graph to be a triple (C,R,S) such that (C,R) is a connection graph (in the hitherto sense) and (C,S) is an S-graph. For such a graph we can define a new kind of subsumption: a clause C subsumes an R-link (Dl'K 1 ,D 2 ,K 2 ),if c subsumes the resolvent of (Dl'K 1 ,D 2 ,K 2 ). It is possible to extend the test to cover this kind of subsumption (see [E80]).

Deleting subsumed links has the effect as if all resolutions leading to subsumed re­ solvents were performed prior to other steps. This results in a stronger reduction of the graph as in the usual case were sub­ sumptions occur only randomly. The diff~ is similar to the one between deleting tautology clauses and deleting tautology links in a graph [WA81].

5. CONSISTENCY OF THE CONNECTION GRAPH PROCEDURE WITH SUBSUMPTION

The soundness of a proof procedure guarantees that whenever an unsatisfiable set of clauses (e.g. one containing o) is derived, then the original set of clauses was unsatisfiable. Consistency, on the other hand, assures ~t from an unsatisfiable set of clauses only unsatisfiable sets of clauses can be de:o:-ived. Thus consistency is a necessary condition for completeness.

In most resolution based proof procedures consistency is trivial, because the original set of clauses is only extended by further clauses. In the case of the connection graph procedure, however, clauses can be deleted from the original set. This fact causes consistency to be an extraordinarily hard problem for connection graphs.

In [EBO] the consistency of all deletion rules mentioned in the introduction is proven for a-derivations [SS76], using a proof technique introduced in [B79]. Un­ fortunately this technique is not suitable to arbitrary derivations, but results shown in [SS76] indicate that there is a translation between a-derivations and ar­ bitrary ground case strategies. The res­ pective proofs are very complex and hard to follow, but if extended to the case of subsumption they might ensure the con­ sistency for the ground case.

In the general case, however, the connection graph proof procedure with unrestricted subsumption is inconsistent as the following example shows:

The resolvent of link 1 is a tautology, the resolvent of link 2 is subsumed by c 1 ,thus both links are deleted and the graph becomes

Resolution on links 3, 5 and the successor of 6 (in that order) will yield the empty clause. Hence the original set of clauses was unsatisfiable, because of the soundness of the resolution principle. If instead of that we select link 4 for the next step, the resolvent is PuPv with link 3 and 5 inherited. This resolvent suhsumes both c 2 and c 3 , which are deleted. The resulting graph is

Now C contains a pure literal and the sub­ sequent deletions finally erase the entire graph, i.e. it is possible to derive a satisfiable set of clauses from the original unsatisfiable set!

This result demonstrates the necessity of restrictions for the deletion rules. It has yet to be shown which restrictions preserve consistency and completeness.

6. PRACTICAL RESULTS

The S-link test has been implemented in the Markgraf Karl system at the University of Karlsruhe [ESSUWBO], [SSBOJ, [ESSWBl]. Sub­ sumption was restricted such that a resol­ vent may not be subsumed by its own parent clauses. The necessity of this restriction appears plausible, because a similar one applies to factors. No example for the in­ consistency of the procedure with this restriction could be found thus far, but neither has there been a formal proof of its consistency.

On the average a graph has about the same number of S-links as it has R-links. This may seem an inappropriate increase in storage requirement. But in the actual implementntion S-links need much less storage than R-links. Moreover, it is not the physical storage that is important, but the number of active R-links in the search space, and this number can be reduced con­ s iderably.

Practical tests indicate that the reduction of the graph caused by subsumption usually more than compensates for the storage used by the S-links. An example is P. Andrews' "challenge" proposed at the deduction work­ shop in Austin 1979: (3xQx= VyQy)"'

( 3xvy = Qx = . Qy) . Here subsumption reduces the initial graph by 89 % of the clauses and by 99,5 % of the R-links (which is, however, an extreme case).

In order to get some experience with more "natural" problems, a selection of examples from [MOW76] and [WM76] was run using the strategies basic resolution, set-of-support, and unit refutation, each with and without subsumption. The values compared are:

G-penetrance

D-penetrance

R-value

~ clauses in proof

# clauses generated

~ Resol vents/Factors in proof

# Resolv./Fact. totally deduced

~ clauses deleted

# clauses generated

The results are compiled in table 1 (-means that the system cid not find a proof).

The table shows that subsumption usually caused a considerable improvement of the penetrances, i.e. fewer unnecessary steps were performed. This demonstrates the re­ duction of the search space. Sometimes the system even found a proof where it did not without subsumption. The increase of the R-value indicates that subsumption infact has a very strong impact on the size of ~ graph.

7. CONCLUSION

The s-link test is a rather efficient sub­ sumbtion criterion and the practical re­ sults are encouraging. The hard theoretkal problem of consistency and completeness of the connection graph procedure with various combinations of deletion rules has yet to await a comprehensive treatment.

B. ACKNOWLEDGEMENT

The members of the Mafkgraf Karl Group in Karlsruhe provided many valuable discussions about the S-link test. Jorg Siekmann and Jack Minker went over the first draft of this paper and gave many helpful hints for its improvement.

table 1

RE FI:R::~:CES

• [ AN79] P. Andrews: Theorem Proving via General Ma­ tings, JACM, vol 28 , no 2 , 1981
• [B79] W. Bibel: On Matrices with Connections, Univ. Karlsruhe, 1979
• [ B75] M. Bruynoogre: The Inheritance of Links in a Connection Graph, Rep. CW2 , Kath. Univ. Leuven, 1975
• [CL7 3] C.L. Chang, R.C .T. Lee: Symbolic Logic and Mechanical Theorem Proving, Acad. Press, New York , 1973
• [ESO] N. Eisinger: Connectionsgraphen und Subsump­ tionsregeln, Diplom thesis, Univ. Karlsruhe, 1980 (in German)
• [ESSUW80] N. Eisinger, J. Siekmann, G. Smolka, E. Unvericht, C. Walther : The Markgraf Karl Refutation Procedure, Proc. of AISB Conf., Amsterdam, 1980
• [ESSWK81] N. Eisinger, J. Siekmann, G. Smolka, P. Kursawe: The Markgraf Karl Refutation Pro­ cedur e: USER MANUAL, Univ. Karlsruhe, 1981
• [ESW78] N. Eisinger, J. Siekmann, G. Wrightson: Paramodulated Connection Graphs, Proc. of the AISB/ GI Conf., Hamburg, 19 78
• [H77] G. Huet: Confluent Reductions: Abstract Pro­ perties and Applications to Rewrite Systems, IRIA lab.,Rapp.deRecherche no 250, 1977
• [K75] R. Kowalski: A Proof Procedure Using Connec­ tio n Graphs, JACM, vol 22, no 4, 1975
• [L78] D. Loveland: Automated Theorem Proving: A Lo­ gical Basis.Fundamental Studies in Computer Science, North-Holland, 1978
• [LS75] M. Livesey, J . Siekmann: Termination and De-
• cidability Results for String Unification, Essex Univ. Memo CSM-8-75, 1975
• [MOW76] J.McCharen, R. Overbeck, L. Wos: Problems and Experiments for and with Automated Theo­ rem Proving Programs, IEEE Trans. on Comp., vol C-25, no 6, 1976
• fR65] J.A. Robinson: A Machine-Oriented Logic Based on the Resolution Principle, JACM,vol 12, 1965
• [ SH76] R.E. Shostak: Refutation Graphs, J. of Art . Intelligence, vol 7 , no I, 1976
• [ SI76] S. Sickel: A Search Technique for Clause In­ terconnectivity Graphs, IEEE Trans. on Comp., vol C-25, no 8, 1976
• [SS76] J. Siekmann, W. Stephan: Completeness and Soundness of the Connection Graph Proof Pro­ cedure, Univ. Karlsruhe, 7/76, 1976
• [SSSO] J. Siekmann, G. Smolka: Selection Heuristics, Deletion Strategies and Terminator Configu­ rations for the Connection Graph Proof Pro­ cedure, Univ. Karlsruhe, 198o
• [SS81] J. Siekmann, W. Stephan : Completeness and Consistency of the Connection Graph Proof Procedure, t o appear 198 1
• fWA8 1] C. Walther: Elimination of Redundant Links in Extended Connection Graphs, Proc. of GWAI-81, Springer Fac hberichte, 1981
• [W~~76] E. Wilson, J. Minker: Resolution, Refinements and Search Strategies; A Comparative Study, IEEE Trans. on Computers, vol C-25, no 6, 1976