Path Resolution with Link Deletion

1. Introduction

Since about 1960 most of the effort in automated deduc­ tion has been concerned with refutation systems. The initial emphasis was on Prawitz analysis [7,9,10,12,20], in which the unsatisfiability of a sentence is deduced without inferring oew formulas. By 1965, with the advent of resolution and (later) paramodulation, the emphasis shifted almost completely toward the use of inference [15,2.1,22,23,27]. Most of the work done within both schools of thought employed conjuoctive or disjunctive normal form. More recently there have beeo adap­ tations of both techniques toward the use of unnormalized or less-normalized formulas [2 ,11 ,16,17,19,25,26].

We introduce a new rule of inference, path resolutioo, w hieb operates on a graphical representation of quantifier-free predicate calculus formulas. The new rule is an amalgamation of resolution and Prawitz analysis . Our goal in the desigo of path resolution is to retaio some of the advaotages of both Prawitz analysis and resolution methods, aod yet to avoid to some extent their disadvantages.

The main advaotage of Prawitz analysis is that, except for variants of original formulas, no new formulas are inferred w hieb rapidly expand the search space. However, except for adding variants, Prawitz analysis is an all or nothing time­ hound search for a contradiction . In contrast, resolution aod other ioference based methods store the progress made at each inference by retaining the inferred formula . Eventually local­ ized cvidence of a cootradiction is produced (usually the empty clause). The required multiple variants of formulas are automatically (and often excessively) generated. But each new formula iotroduced interacts with others, expanding the search rapidly in both time and 8pace.

Ooe of the disadvantages of resolution is its reliance oo coojunctive normal form. We avoid conjuoctive aod disjuoc­ tive normal form and the duplication of literals that their use and Erik Rosenthai University of New Haven Department of Mathematics West Haven, CT 06516

may necessitate, since path resolution operates oo formul as in negatioo normal form. We have found that the aoalysis is greatly simplified by a represeotation of NNF formulas which we call semantic graphs.'

Path resolutioo allows Prawitz aoalysis of an arbitrary subgraph of the existiog graphical represeotatioo of formul as. If such a subgraph is not !arge eoough to demoostrate a con­ tradiction, a path resolveot of the subgraph may be geoerated with respect to the. entire graph. Path resolutioo operations include (properly) all resolutioo-based infereoces of which the authors are aware, such as hyper-resolutioo, clash-resolutioo , NC-resolution, aod UL-resolution.

It will be obvious to the informed reader that the work reported here, while new, has been syothesized from a oumber of importaot ideas developed by others. The most iofluential of these are Robioson's clash resolutioo [24], Kowalski 's connection-graph procedure [14], the work of Andrews [2] and Bibel [3,4] on paths, matrices, aod thP. spaoning property, and the non-clausal systems of Stickel [25] and of Waldinger and Manna [26] .

In the next section we introduce the ootation and termi­ nology required for expressing formulas and their semantics in terms of semaotic graphs and paths . We further develop this formalism in section 3; sectioo 4 introduces the rule of infer­ ence, path resolutioo. Section 5 contaios a sample refutation , aod section 6 introduces two link deletioo strategies. We omit maoy proofs for Iack of space; they are available in [18].

2. Semantic Graphs and Paths

A umantic graph is a means of represeotiog a logical for­ mula, and paths determine the semantics of the graph. We assume that the reader is familiar with the definitions of atom, Iitera/, formula, resolution, and unification. We will consider only quantifier-free formulas in which all negatioos are at the atomic Ievel.

A semantic graph is empty, a siogle node, or a triple {N,C,D} of nodes, c-arcs, aod d-arcs, respectively, where a node is a Iitera! occurrence, a c-arc is a conjuoction of two oon-empty semaotic graphs, aod d-arc is a disjunction of two non-empty semaotic graphs. Piease note that a node is a Iitera! occurreoce, so that if a Iitera! occurs twice in a form ula, we will Iabel both oodes with that Iitera!. Each semantic graph used in the constructioo of a semaotic graph will be called an explicit subgraph, aod we shall insist that each proper explicit subgraph be cootained in exactly one arc. We will use the notation ( G ,H )c for the c-arc from G to H and similarly use ( G ,H )d for a d-arc. The subscript may be omitted if there is no possibility of coofusioo , aod we will use the term graph only for semaotic graphs.

We will consider an empty graph to be an empty disjunc­ tion, which is a contradictioo. A coostructioo of a graph may be thought of as a sequeoce of c-arcs aod d-arcs . There will always be exactly one arc (X, Y) with the property that every other arc is an arc in X or in Y. We call this arc the final arc of the graph, and X and Y are the final aubgrapha. Since this arc completely determines G, we frequently write G =(X , Y ).

As an example, the formula

is the graph

Note that horizontal arrows are c-arcs, and vertical arrows are d-arcs. There are two d-arcs: (A -+ B,C) and ( A, D -+ C); and there are three c-arcs: (A,B), (D,C), and the entire graph. Some of the explicit sub­ graphs are each of the nodes, A -+ B, and the right-hand part of the graph.

The formulas we are considering are in negation normal form (nnf) in that all negations are at the atomic Ievel, and the only connectives used are AND and OR.

If A and B are nodes in a graph, and if a = (X , Y) is an arc ( c- or d-) with A in X and B in Y, we will say that a is the arc connecting A and B. If a is a c-arc, we will say that A and B are c-connected, and if a is a d-arc , we will say that A and B are d-connected.

Lemma 1. Let G be a semantic graph, and Iet A and B be nodes in G. Then there is a unique arc connecting A and B.

One of the keys to our analysis is the notion of path. Let G be a semantic graph. A partial c-path through Gis a set c of nodes such that any two are connected by a c-arc. We allow the empty set or a singleton set to be a partial c-path. A c­ path is a partial c-path which is not properly contained in any partial c-path. Notice that any partial c-path is extendible to a c-path, and hence partial c-paths are always subpaths of c­ paths. We similarly define d-path using d-arcs instead of c­ arcs . The next Iemma is an immediate consequence of Lemma 1.

Lemma 2. If A and B are nodes in a graph G, then there is a c-path or a d-path (but not both) containing A and B.

Using paths, we can define the conjunctive normal form of a graph as the conjunction of the d-paths, and the disjunc­ tive normal form as the disjunction of the c-paths. If a for­ mula is multiplied out using the distributive laws, then the graph changes and so may the normalized formso

Paths can be defined in a somewhat more structural mannero Define a atructural c-path (scp) c in a graph Gas fol­ lows: if G consists of a single node A, then c is the set {A}; if the final arc of G is a d-arc, then an scp in G is an scp in one of the final subgraphs; and if the final arc is (X, Y) c· then c is the union of an scp in X and an scp in Yo Lemma 3 states that the two formulations of path are equivalent, and as a result we will abandon the terminology structural c-path after the Iemma.

Lemma 3. Let G be a semantic graph and Iet c be a set of nodes in Go Then c is a c-path iff c is an scpo

There is an obvious similar statemcnt about d-paths; we leave the proofs to the reader o

The proofs of Lemmas 1 and 3 and of many Iemmas and theorems that follow often use induction on the number of arcs in the grapho The base case is always trivial since the graph will then consist of a single node or arc. Since each explicit subgraph will always have fewer arcs than the entire graph, the inductive hypothesis amounts to assuming that the result holds for all explicit subgraphso As a result , in proofs we do include in this paper, we will ignore the base case and begin by assuming that the result holds for all explicit sub­ graphs.

We will use the notation c = xy w hen two paths in sub­ graphs are put together to form a path in a graph as in the Iemma.

Lemma 4. Let G be a semantic graph. Then an interpretation I satisfies (falsifies) G iff I satisfies ( falsifies) every literal on some c-path (d-path) through G.

We will frequently find it useful to consider subgraphs w hieb are not explicit; that is, given any set of nodes, we would like to define that part of the graph which consists of exactly that set of nodes . The previous example is shown below on the lefto The subgraph relative to the set {A, C, D} is the graph on the right.

If N is the node set of a graph G, and if N 1 is con­ tained in N, we define GN , , the aubgraph of G relative to N 1 as follows: If N 1 = N; then GN ' = G o If the final arc of Gis (X, Y) , and if the nodes in N 1 all appear in X or in Y, then GN ' = XN ' or GN ' = Y N , , respectively . Otherwise, GN ' = (XN ' , YN ' ), where this arc is of the same type as (X, Y). The following Iemma says in essence that the subgraphs we have defined are the objects we want .

Lemma 5. Let G be a semantic graph with node set N, and Iet N 1 be a subset of N. Then

i) Every node in N 1 is a node in some arc in G N, o

• ii) If p 1 is a path through G N' , then p 1 is the restriction to N 1 of a path p (of the same type) through G; in par­ ticular, if p 1 is a partial path in G consisting of nodes from N 1 , then p 1 is a partial path in G N, o

3. Blocks

Consider the graph (A -+ B) -+ C. The non-explicit sub­ graph B -+ C "feels" much like an explicit one, and certainly the graph A -+ (B -+ C) is essentially identical to the original grapho Indeed, the graph A -+ C is an explicit subgraph of another essentially identical graph: (A -+ C) -+ Bo Subgraphs with this property can be characterized with the notion of blocko A c-block Cis a subgraph of a semantic graph with the property that any c-path which includes at least one node from C must pass through C; that is, the subset of the c-path consisting of the nodes which are in Cis a c-path through Co A d-block is similarly defined with d-paths, and a full block is a subgraph which is both a c-block and a d-blocko From Lemma 4 we know that the c-paths through a graph. determine the semantics of the graph, and that the d-paths also determine the semanticso This might Iead one to believe that c-blocks and d-blocks are full blockso This is not the case, as the fol­ lowing simple example illustrates:

B C

The subgraph relative to {A,B} is obviously a c-block, but it is not a d-block since {A C} is a d-path which meets the sub­ graph but does not pass through ito

We define a 1trong c-block in a semantic graph G to be a subgraph C of G with the property that every c-path through G contains a c-path through Co A 1trong d-block is similarly defined.

Lemma 6. If C is a c-block in a semantic graph G, if the final arc (X, Y) of Gis a c·arc, and if C meets both X and Y, then C is a strong c-block. Moreover, the subgraphs C x and C y, consisting of the intersections of C with X and Y, are themselves strong c-blocks.

Lemma 7. The union of any num her of d-paths in a semantic graph G is a strong c-block. Conversely, a d-path. through a strong c-block is a d-path through the entire graph.

Lemma 8. If C is a c-block in G, and if d 1 ,d 2 , ... ,dk are d-paths through C, then their union is a c-block in G.

It is obvious that explicit subgraphs are full blocks. There is a sense in which the converse is true. Define two graphs (N, C, D) and (N 1 , C 1 , D 1 ) to be iaomorphic if there exists a bijection f: N -+ N 1 such that for each A in N, A=f(A), and which preserves c- and d-paths. (By A=f(A), we mean that A and f(A) are the same Iitera!. It is not at all clear what one would even mean by saying that A and f(A) are the same node since they appear in different graphs .) The con­ dition A=f(A) is an essential part of the definition· otherwise the graphs A -+ B and C -+ C would be isomorpllic. Notic~ that being isomorphic is obviously an equivalence relation. A simple example of isomorphic graphs is A -+ (B -+ C) and (A -+ B) -+ C with the "identity" map.

One method of obtaining an isomorphic image of a graph is through comm utivity and associativity. Commutivity in a graph amounts to reversing the order in which an arc is formed; e.g., ( Y,X)c instead of (X, Y)c. Associativity in graph amounts to changing the order in which two arcs of the same type are formed; e.g., (X ,( Y, Z)clc instead of ((X, Y ) 0 Z Je It is immediate that two graphs w hieb are identical except for one such commutation or one such reassociation are iso­ morphic. Since being isomorphic is transitive , any nurober of commutations and reassociations will result in an isomorphic graph. In fact, the converse is true. This, and the fact that full blocks are essentially explicit subgraphs, are corollaries of Theorem 1 below.

We define Ievel in a graph Gas follows: The Ievel of Gis 0 and the Ievel of its final arc is 1. Given an arc a =(X, Y) of Ievel k, if the final arc of Xis of the same type as a then that final arc has Ievel k; otherw ise it · has Ievel k+ 1. In either case the Ievel of Xis k.

Theorem 1. Let G be a semantic graph, and Iet B be a full block in G. Then B is a union of Ievel 1 subgraphs of an explicit subgraph of G.

Proof. By induction on the nurober of arcs in G. Let the final arc of G be (X, Y) and assume that (X, Y) is a c-arc; the case for a d-arc is similar. If Bis a subgraph of X or of Y, the induction hypothesis applies, and the theorem holds.

So suppose some nodes of B are in X and some are in Y; recall that B x and B y are the subgraphs of B consisting of the nodes of B which are in X and of those which are in Y, respec­ tively. We show first that Bx and By are themselves full blocks. It is obvious that each is a d-block since the arc (X, Y) is a c-arc: any d-path through G is a d-path through X or a d-path through Y. To see that Bx is a c-block in X, note that Bis a strong c-block by Lemma 6. Hence by Lemma 7, Bis a union of d-paths through G. Thu~ B x is a union of those d­ paths which lie in X; i.e., Bx is a strong c-block in X and in particular a full block in X. Similarly, By is a full block and strong c-block in Y.

Now, if the final arc of X is a d-arc, then B x meets both final subgraphs of X and hence is a strong d-block in X. Since it is both a strong c-block and a strong d-block it must be all of X.

If the final arc of Xis a c-arc, Iet U be any Ievel I sub­ graph of X which meets Bx. The proof will be complete for B x ( and by symmetry for B y and hence for all of B) if we show that U C Bx. But this is clear since the final arc of U must be a d-arc; i.e., the proof is identical to the case when the final arc of Xis a d-arc .

Corollaries 1, 2, and 3 are immediate consequences of the theorem. The first corollary (and its generalization, Corollary 4) and the theorem are especially important. Because of the chronological order in which they were originally proven, we will refer to Theorem 1 as the aecond iaomorphism theorem and to Corollaries 1 and 4 as the firat iaomorphiam theorem.

Corollary 1. Let G be a semantic graph , and Iet B be a full block in G. Then there is a semantic graph G 1 and an isomorphism f: G-+ G 1 such that f(B) is an explicit sub­ graph of G 1 ·

Corollary 2. If G and H are isomorphic semantic graphs, then H can be formed by reassociating and commuting some of the arcs in G.

Corollary 3. The intersection of two full blocks is a full block.

Corollary 4. Given a semantic graph G and a collection of mutually disjoint full blocks , there is a graph isomorphic to Gin which each full block is an explicit subgraph . Moreover, given any two of the blocks, each node in one is c-connect.ed to each node in the other or each node in one is d-connected to each node in the other.

We will find it useful to determine the smallest full block containing a given subgraph; to do that we need the notions of c- and d- extenaion. The c-extension and the d-extension of the entire graph G is G itself. Given a Ievel k subgraph X in G, if (X, Y)c is an arc in G, then the c-extension of X is the (unique) Ievel k-1 subgraph containing X, and the d-extension is X. The obvious dual applies for (X, Y)d. Given an arbitrary subgraph Hof G, to find the smallest full block containing H, Iet k be the smallest integer such that more than one Ievel k subgraph of G meets H. (Note that k must exist unless H con­ sists of a single node, in which case His a full block.) Then the smallest full block containing H is the subgraph consisting of those Ievel k subgraphs which meet H.

lt will be useful to divide an arbitrary subgraph Hof a graph G into c-blocks. We define a c-block C contained in a subgraph H to be maximal if no superset of C in H is a c­ block. The c-blocks in the definition are assumed to be c­ blocks in G, which trivially implies that they are c-hlocks in H. But note that if His not a full block, a subgraph which is a c­ block in H might not be a c-block in G. In particular, H may not be a c-block and typically will not be. We define a proper c-family of H to be a collection of maximal c-blocks whose union is H. The members of a proper c-family are not in gen­ eral disjoint.

The next theorem says in essence that a certain r ule of inference is sound. This may not be entirely obvious from the statement, w hieb is purely structural. First, define the auxili­ ary aubgraph Aux(H,G) of a subgraphHin a semantic graph G to be the subgraph of G relative to the set of all nodes in G w hieb lie on extensions of d-paths through H to d-paths through G. The proof of the next Iemma is immediate.

Lemma 9. If His a subgraph of G, then Aux(H,G) is empty iff His a strong c-block. Moreover, Aux(H,G) cannot contain a d-path through G; if H is a c-block, then so is Aux(H,G).

Theorem 2. Let { C 1, C 2, ... , Cd be a proper c-family in a subgraph H of a graph G. Let I be an interpretation w hieb satisfies a c-path p through G, and suppose that p does not pass through H. Then I satisfies Aux( C; ,G ) for some i.

Proof. Since p does not pass through H, it must fail to pass through Ci for some i. Hence, p must entirely miss Ci , and so p must meet and hence pass through Aux( Ci ,G ). · Example 1:

Let S be the subgraph relative to {A, B, C, A, B, C}. S may be partitioned into the following four c-blocks: {C, B}, {A}, {B}, and {C, A} . However these are not maximal; in particu­ lar, the last two c-blocks may be combined to form {C, B}, {A}, and {B, C, A}. But we still do not have a proper c­ family. The c-block {A} is not maximal because the node B can be added and {A, B} is still a c-block; {C, B}, {A, B}, and {B, C, A} do form a proper c-family.

Under the conditions of Theorem 2, it is immediate that the disjunction of the auxiliary subgraphs is satisfied by I. (In the above example, any c-path that misses the first c-block must hit subgraph {Q, P}. A c-path missing the second c­ block hits {P}, and one missing the third c-block hits {R} .) We denote this disjunction by P(H, G). We shall soon see that there are redundancies built into P(H,G) which can be elim­ inated. These redundancies arise from the fact that the auxili­ ary subgraphs need not be disjoint. Theorem 3 indicates how to remove them. First, define a subgraph of a graph G to be a d-full block if it is a full block and a strong d-block. Note that for H to be a d-full block in G, H must be a disjunction of one or more Ievel 1 subgraphs of G.

Theorem 3. Let { C 1 , . ·. ,C k} be a proper c-family in a subgraph Hof a semantic graph G, and Iet K be the intersec­ tion of Aux( Ci ,G) and Aux( Ci ,G ). Then K is empty or a d­ full block in A ux( Ci , G ).

The significance of Theorem 3 is that the redundancies which appear in P(H, G) are its Ievel 1 subgraphs which appear more than once. In example 1, the auxiliary subgraphs of the intersecting c-blocks are the subgraphs relative to {P, Q} and {P}. Their intersection is of course the node P which forms a Ievel 1 subgraph in both auxiliary subgraphs and in their dis­ junction. However, we can form the disjunction of auxiliary subgraphs to build P(H,G) and leave out the redundancies ; i.e., use the intersections of the auxiliary subgraphs only once. We denote the resulting graph by Q(H,G). We prove that Q(H,G) is unique by defining an object WS(H, G), the weak ßplit graph of Hin G, and showing that WS(H,G) = Q(H,G). (We intro­ duce ßtrong split graph in section 6.) We define WS(H, G) as follows :

WS(H,G) = WS(Hx,X) V WS(Hy,Y) if G =(X, Y)c and H meets both X and Y.

WS(H ,G)=WS(Hx,X)(orWS(Hy,Y)) if G = (X,Ylc and His contained in X (in Y, respectively)

We will write WS(H,X) for WS(H x,X ). Notice that no nodes appear more than once in WS(H,G), and that WS(H,G) is uniquely defined. In Theorem 4, we show that Q(H,G) = WS(H,G), which teils us that Q(H,G) can be computed without first discovering a proper c-family.

Theorem 4. If H is a subgraph of a semantic graph G, then Q(H,G) = WS(H,G).

lt should be noted that only structural redundancies are eliminated by weak split; it is certainly possible that the literals which occur in Gwill result in WS(H,G) being a tautol­ ogy. In view of Theorem 4, we will use only the notation WS(H, G). The following corollaries are immediate.

Corollary 1. Let H be a subgraph of a graph G, and Iet be an interpretation which satisfies a c-path p through G. Then if p does not pass through H, I satisfies WS(H, G).

Corollary 2. If H is a c-block in a graph G, then WS(H,G) is isomorphic to Aux(H, G).

4. Path resolution.

The discussion of paths and graphs gives a (we think use­ ful) representation of logical formulas as graphs. The primary concern of this paper is path reßolution, a rule of inference. To this end, we define a chain in a graph to be a set of pairs of c-connected nodes such that each pair can simultaneously be made complementary by an appropriate substitution. A link is an element of a chain, and a chain is full if it is not prop­ erly contained in any other chain. A graph G is ßpanned by the chain K if every c-path through G contains a link from K. Notice that if a graph is spanned by a chain, the graph must be a contradiction since no c-path w hich contains complemen­ tary nodes can be satisfied. If K is a chain, we use the nota­ tion GK for the subgraph of G relative to the set of nodes w hich appear in K. If G K is spanned by K, K is said to be a reßolution chain, and G K is said to be a resolution ßubgraph. Example 2:

The curves between A and A and between B and B represent links which form a chain. The subgraph relative to the chain JS:

The c-paths are {B A A} and {B A B} . Each obviously con­ tains a link, so we have a resolution chain and a resolution subgraph.

A rule of inference is of course a procedure which pro­ duces a formula from a given formula, and such a procedure is sound if any interpretation which satisfies the original formula also satisfies the inferred formula. Resolution is such a rule; in essence, it applies to formulas in cnf and operates on chains consisting of a single link. We will define a generalization of resolution which we call path reßolution. lt applies to any semantic graph and operates on arbitrary spanning chains.

Let K be a resolution chain in a semantic graph G, and Iet R = GK . If I is any interpretation which satisfies G, it satisfies a c-path through G. Since R cannot be satisfied, c cannot pass through R. Hence, by Theorem 4, I mußt ßat14y WS(R,G) . We call WS(R,G) the path reßolvent of R in G, and we have

Theorem 5. Path resolution is a sound rule of inference.

Consider Example 2 again. We have already seen that

is a resolution subgraph. The c-blocks are [B -+ A] and the d-path {A, B}. The auxiliary subgraph of the second is [C -+ E] since the (partial) d-path {A D} does not pass through the resolution subgraph. The path resolvent is

Once aresolvent has been inferred, it may appear natural to conjoin it with G. There is a better way to handle this: the split subgraph should be formed in the smallest full block M containing the resolution chain R, and the resolvent should then be conjoined to M rather than to all of G. That is, we replace M in G with (M, WS(MR , M ))c. We will call the resulting graph the weak re8ultant of G with re8pect to R and denote it WRes( G,R). In the previous examples, ( and quite often in gene.ral,) M is a union of Ievel 1 c-connected subgraphs of G, and therefore WRes( G,R) = ( G , WS( R , G ))c.

5. A Refutation Proof

Consider the following formulas taken from Chang and Lee [5].

1. 't;Jx (P(x) => ~V(x))

We wish to show that (1), (2), and (3) imply (4) below.

1. 3x (P(x) 1\ C(x))

The semantic graph for (1), (2), (3), and the denial of (4) is shown below. Notice that the node !5"(XJ is derived from the atom P(x) in both (3) and the denial of (4) . If we bad represented (3) and ~(4) as separate c-connected graphs, the proof below would still go through; links 3 and 5 would simply contain different occurrences of !S"(XJ.

Links 1, 2, and 3 span their associated subgraph and therefore form a resohition chain. The weak split of this chain with respect to the entire graph is the graph S(a,f(a)) -+ C(f(a)). We show this path resolvent below along with a portion of the original graph:

Resolving on links 4 and 5 yields V{1(a}) -+ cmaJ'j.

It is now easy to see that the link {cmaJ), C(f(a))} is a resolu­ tion chain that spans not only its subgraph but the entire graph. Therefore this link produces the empty graph upon activation. The careful reader may have noticed that this last link is inherited from {C(X}, C(f(a))} which could have been added to the resolution chain used in the second inference. The resulting chain would have produced a contradiction shor­ tening our proof to two steps. A binary resolution refutation for these formulas given in [5] uses eight steps.

We do not claim that the search space for determining an appropriate resolution chain is small. However, the existence of a 2-step derivation for this example is certainly somewhat favorable. Moreover, we note that both path resolution steps admit link deletion under certain extensions of Theorems i and 8. Space limitations preclude discussion of those exten­ sions here. A derivation of a logic program by NO-resolution is compared to a derivation of the same program by path reso­ lution in [18].

Stickel [25] has pointed out that in a non-clausal connec­ tion graph system it may be wise to avoid inferences on non­ atomic complementary subformulas. Two reasons cited are that complementary subformulas may be difficult to detect , and that such inferences may be duplicated by resolving on single literals only. Path resolution may help to solve both of these problems. We only link atoms and their complements, not non-atomic structures. The presence of complementary subformulas is detected by a resolution chain. The subformula relative to a resolution chain is frequently (but not always!) a conjunction of complementary subformulas comprised of the literals appearing in the chain, even though these literals may be scattered throughout the entire sentence.

8. Link Deletion

Path resolution is so general that it admits as special cases all resolution-based inference rules (e.g. hyper-resolution, clash resolution UL-resolution, NO-resolution) of which the authors are aware. In fact, if enough copies of formulas from an unsatisfiable set are represented, then a resolution chain will exist whose path resolvent is the empty d-path. We may therefore view semantic graphs and path resolution as a uni­ fying framework for all resolution-based inference and Prawitz analysis.

This generality is elegant from a theoretical point of view, but it also admits a proof-search space I arger even than that of unrestricted binary resolution. It is natural to ask w hether restrictive strategies exist that would take advantage of path resolution's generality, and not just mimic known stra­ tegies applicable to (say) clausal logic. One natural restriction is to !arge chains; that is to avoid resolution chains that are proper sub-chains of currently known resolution chains. Our intuition is that such a strategy is favorable for refutations , and this is an area of ongoing investigation.

Another way to reduce the search space is to delete links after activation. In [3] and [4], for example, Bibel dealt with these issues within binary resolution. We develop two link deletion strategies for path resolution below.

6.1. Link deletion using full blocks

It is more or less the case that a necessary and sufficient condition for a link deletion strategy to be acceptable is that the spanning property be preserved. That is, if a graph is spanned by a set of links, and if a rule of inference which deletes links is applied, then the resulting graph should still be spanned. Theorems 7 and 8 introduce classes of resolution chains for which path resolution has this property. Theorem 6 gives a condition when certain links can be deleted. It should be pointed out that since we are considering link deletion, we will not in general be dealing with the full set of links, and we will not need to inherit all links. lf L is the current set of links in a graph G, and if R is the resolvent with respect to a resolu­ tion subgraph of the form ( U, V)c such that the conditions of Theorem 7 or 8 are satisfied, then we need not inherit any links from U or from V to R. The reason is that the only paths in the new graph we need be concerned about are those w hieb pass through ( U , V Je; in Theorems 7 and 8 we essen­ tially show that extensions of such paths through R m ust con­ tain an inherited link, and this allows deletion of the links in R.

Recall that any full block U is a conjunction or a disjunc­ tion of Ievel I subgraphs of some explicit subgraph H. If the final arc of H is a conjunction, then the c-extension of U is H and the d-extension of U is U itself. The situation is reversed if the final arc of His a d-arc . We will use the notation CE( U) and DE( U) for the c- and d-extensions, respectively, of U.

Lemma 10. Let U be a full block in a graph G whose final arc is a c-arc. Let Z1 = CE( U) and U 0 = U , and for i 2': I define Zi , Yi , and Ui recursively as follows: Yi = DE(ZJ, Zi =CE( Yi_d, and Ui = Yi - Zi. Then

1. Either Z 1 = G or there exists an m such that Zi= Yi=Giffi2':m.

ii) lf p is a c-path through G, then there exists a k such that p passes through U k but completely misses U i for i < k. (We do not exclude the possibility that p passes through U, i.e., that k = 0.)

Proof. The proof is actually fairly trivial. Observe that each Z i is a Ievel 1 subgraph of Y i· and that each Y i is a Ievel I subgraph of Zi+1. Observe further that Ui is the full block consisting of the disjunction of the Ievel 1 subgraphs of Y i different from Z ,. To see that i) holds, note that if Z 1 is not all of G, then Y m- 1 is the Ievel 1 subgraph of G containing U. To see that ii) holds, note that there is at least k such that p passes through Y k· Then p misses Zi for i ::; k. · Example 3:

B

Let U 0 be the (subgraph relative to) the single node A w hich is obviously a full block. Then, as defined in Lemma I 0, Z1 = {A}, Y1 = DE({A}) = {P, A} , U1 = Y1 - Z1 = {P}, Z2 = CE(Y1) = {Q, P, A}, Y2 = DE(Z2) = {Q, P, A, B}, U2 = Y2 - Z2 = {B}, and Z3 = CE(Y2) = the entire graph. Notice that any c-path must pass through U0, U1, or U2 .

Theorem 6 is a generalization of Bibel's Pure Lemma [3] .

Theorem 6 . Let U be a full block in a semantic graph G, Iet L be a set of links, and suppose that no node in U is contained in a link from L. Let L 1 be the set of links from L w hieb do not contain a node from DE( U). Then G is spanned by L iff G is spanned by L 1 ·

Proof. Since L 1 is a subset of L, we need only consider the case when G is spanned by L. If DE( U ) = U, then L 1 = L, and there is nothing to prove. If not, Iet D = DE(U) and U 1 = D - U; Iet p be a c-path through G. We must show that p contains a link from L 1 · If p does not pass through U 1 , there is nothing to prove since the links deleted from L all contain nodes from U 1 · If p does pass through U 1 , Iet p = r 1 s, w here r 1 is a path through U 1 and s is the rest of p. Let r be any c-path through U. Note that every node in s is c-connected to all of D since D is a full block and the nodes of s are c-connected to some nodes in D (namely, those in r 1 ) . Then rs is a c-path through G and must contain a link from L. This link is in L 1 since no link in L contains a node from U which contains r. This com­ pletes the proof since this link must be in s and therefore in p. ·

The next theorem gives a condition und er w hieb links may be deleted. lt says that if ( U, V )c is a resolution sub­ graph in which U and V are each full blocks in G, and if the links in the chain all go from U to V, then we may delete all links from U to V.

Theorem 7. Let R be a resolution chain in semantic graph G such that G R has the form ( U, V)" w here U and V are full blocks in G, and where each link in R goes from U to V. Suppose further that Gis spanned by a set of links L. Let H = WRes(R, G ), and Iet L 1 be the set of inherited links together with all links in L which do not go from U to V. Then L 1 spans H.

Proof. We proceed by iuduction on the number of arcs in G. The case for one arc is trivial. lf (X, Y)d is the final arc of G, then R must be entirely contained in X or in Y and the induction hypothesis gives the desired result. If the fin al arc is (X, Y)c, and if R is contained in X or in Y, again the induction hypothesis applies. So suppose that the final arc is a c-arc and R meets both X and Y. By the first isomorphism theorem, we may assume that U and V are explicit subgraphs. Hence nei­ ther can meet both X and Y. Assurne that U is contained in X and V is contained m Y. Observe that H = ( G, WS( G R· G ))c-

Let p be a c-path through H. We must show that p con­ tains a link from L 1 · Note that p is the union of c-paths p1,p2,p3 through X, Y, and S = WS(GR,G) , respectively. The only case we need consider is w hen p passes through G R and all links in p1p 2 come from R. Since S is the disjunction of WS( U, X) and WS( U, Y), we assume without loss of generality that p 3 is a c-path through WS( U, X). Since U is an explicit subgraph, we know that its split is isomorphic to Aux( U, X) by Corollary 2 of Theorem 4. Let p3 1 be the isomorphic image of p 3 in Aux( U, X).

Using the notation of Lemma 10, apply part ii) of that Iemma to p3 1 · Since p3 1 passes through Aux( U, X), it misses U and hence k > 0. As in the proof of Lemma 10, Iet p1 = sr, w here r is a c-path through Z k· lt is obvious that sp 3 1 is a path through X, so sp 3 1 p 2 contains a link from L. This link is not in R. Moreover, p 2 misses Aux( V, Y) , so this link will be inherited, and the proof is complete. ·

lt is worth noting that all single link chains satisfy the conditions of Theorem 7, and that the proof for this case is no easier since a pair of linked nodes plays the same roJe structur­ ally as the two full blocks in the theorem.

Consider activating the single-link chain {A, A} in exam­ ple 3. This chain clearly satisfies the conditions of Theorem 7. Notice that the resultant graph is still spanned even though the activated link is deleted:

6.2. Another form of path resolution

Consider the soundness argument for path resolution as defined in section 4. In some cases the c-paths that miss the resolution chain are )arger than the c-paths in the (weak) split subgraph. To account for this we define the 3lrong 8plit of an arbitrary subgraph H in G, SS (H ,G ), to be the same as WS(H, G) with the exception that if G =(X , Y Je and H is contained in X, then SS(H, G) = SS(H ,X) 1\ Y . If R is a resolution chain, Iet M be the smallest full block containing R. lt is Straightforward to verify that if an interpretation satisfies M then it satisfies SS( G R· M ), and hence we may replace M in G with (M , SS(GR, M))c- We call the resulting graph the 8lrong re8ultant of G with re8pect to R, and denote it SRes( G, R) . The following Iemma yields both soundness for strong splits and spanning preservation with link deletion for the class of resolution chains described in Theorem 8.

Lemma 11. If Xis a c-block in G, then SS(X, G) is iso­ morphic to the subgraph of G consisting of all nodes that lie on c-paths w hich miss X.

Proof Suppose first that G = ( U, V )d- Then SS(X, G) = (SS(X , U ), SS(X, V ))d and the result follows from the ind uction hypothesis. If G = ( U , V ) 0 and if X meets both U and V then X is a strong c-block and SS(X, G) is empty. Finally if X is contained in U, then SS(X, G) = (SS(X, U ), V )c and the induction hypothesis applies. ·

Theorem 8 . Let R be a resolution chain in semantic graph G such that G R has the form (X, Y Je, where X and Y are c-blocks in G, and where each link in R goes from X to Y. Let G be spanned by a set of links L, and Iet M = ( U, V )c be the smallest full block containing R, w here U and V are chosen to contain X and Y respectively. Then H = SRes( G, R) is spanned by L - R and the links inherited from L.

Proof Let p be a c-path through H, and Iet M 1 = (M, SS( GR , M))c. If p does not pass through M' , then p misses M' entirely since M' is a full block, so p must have a link from L. Assume p passes through M' . Let p = P1P2P3 where PJ ,P2,P3 are c-paths through U , V, and SS( G R· M) respectively. Since Xis a c-block in U, Lemma 9 applies, so Iet p3 1 be the isomorphic image of p3 in U. Then the c-path p3 1 p2 has a link in L that is not in R and that is therefore inherited . ·

Consider the two-link chain {A, A}, {8, 8}, again from example 3. This chain satisfies .the conditions of Theorem 8, but not those of Theorem 7 because {A, B} is a c-block but not a full block. Shown below is the outcome of act ivating this chain with strong split and deleting both links. Of course the graph is still spanned. But notice that had we used weak split, the resolvent would have included only P, and the c-path {8, 8, A, Q, P} would then be without a link.

7. Summary

We have introduced a graphical representation of formu­ las and a new rule of inference that employs this representa­ tion. The inference rule is path resolution, which is a generali­ zation of most previous forms of resolution. We have demon­ strated the rule's soundness. Completeness is immediate in the absence of the usual connection graph link deletion stra­ tegy; resolving 'exclusively on single-link chains amounts to atomic NC-resolution on nnf formulas. We have introduced two classes of chains for which the activation and subsequent deletion of links is shown to preserve the spanning property. In light of Bibel's results [3,4] such link deletion strategies may reasonably be conjectured complete.

Heferences

1. Andrews, P .B. Refutations by matings. IEEE Transactions on Computers 25,8 (Aug. 1976), 801-807.
2. Andrews, P.B. Theorem proving via general matings. JACM 28,2 (April 1981), 193-214.
3. Bibel, W. On matrices with connections. JACM 28,4 (Oct. 1981 ), 633-645.
4. Bibel , W. A Strong Completeness Result for the Connection Graph Proof Procedure. Technical Report ATP-3-IV-80.
5. Chang, C.L. and Lee, R.C.T. Symbo /ic Logic and Mechanica/ Theorem Proving, Academic Press, New York, 1978.
6. Chang, C.L. , and Slagle, J.R. Using rewriting rules for connec­ tion graphs to prove theorems. Artificial lntelligence 12 (Aug. 1979), 159-178.
7. Chinlund, T .J ., Davis, M., Hineman, P.G., and Mcllroy , M.D. Theorem proving by matching. Bell Labaratory, 1964.
8. Clark, K. The Synthesis and Verificat~on of Logic Programs. Third Conference on Automated Deduct10n, August 1977.
9. Davis, M. and Putnam, H. A computing procedure for quantification theory. JACM, vol. 7 ( 1960), 201-215.
10. Davis, M. Eliminating the irrelevant from mechanical proofs. Proc . Symp. of Applied Mathematics 15 (1963), 15-30.
11. de Champeaux, D. Sub-problem finder and instance checker - two cooperating processors for theorem provers. Proc. 4th Workshop on Automated Deduction, Austin , Texas, Feb. 1979, 110-114.
12. Gilmore, P .C., A Proof method for quantifi cation theory. IBM Journal of Research and Development , vol. 4 (1960) , 28-35.
13. Henschen , L.G. Theorem proving by covering expressions. J.ACM, 26,3 (July 1979), 385-400.
14. Kowalski , R. A proof procedure using connection graphs. J .ACM 22,4 (Oct. 1975), 572-595.
15. McCharen, J., Overbeek, R. and Wos, L. Proble':lls and experi­ ments for and with automated theorem-provmg programs. IEEE Transactions on Computers, C-25,8 (Aug. 1976), 773-782.
16. Murray , N.V. Completely non-clausal theorem proving. Artificial lntelligence 18, 1 (Jan. 1982), 67-85.
17. Murray , N.V. An experimental theorem prover using fast unification and vertical path graphs. Fourth National Conf. of Canadian Society of Computational Studies of lntelligence , U. of Saskatchewan, May 1982.
18. Murray , N. V. and Rosenthal, E. Semantic graphs. Technical Report 84-12, Department of Compu ter Science, SUNY at Albany , Nov. 1984.
19. Nilsson, N.J. A production system for automatic deduction. Technical Note 148, SRI International, 1977.
20. Prawitz , D. An improved proof procedure. Theori a 26 (1960) , 102-139.
21. Robinson, G.A. and Wos, L. Paramodulation and theorem proving in first order theories with equali ty. Machine lnt e//i­ gence 4, 1969, Edinburgh University Press.
22. Robinson, J .A. A machine oriented logic based on the resolu­ tion principle. J.ACM 12,1 (1965), 23-41.
23. Robinson , J.A. Automatie deduction with hyper-resolu tion. International Journal of Computer Mathematics, 1 (1965), 227234.
24. Robinson, J.A. "Theoretical Approaches to Non-Numerical Problem Solving," Springer-Verlag, New York , lnc., 1970, 2-20.
25. Stickel, M.L. A nonclausal connection-graph resolution theorem-proving program. Proc. AAAI-82 Nat. Conf. on Artificial lntelligence, Pittsburgh, Pennsy lvania, Aug. 1082, 229-233.
26. Waldinger , R. and Manna, Z. A deductive app roach to pro­ gram synthesis. ACM TOPLAS 2, 1 (1980) , 90-121.
27. Wos, L., Carson, D. and Robinson, G. Efficiency and complete­ ness of the set of support strategy in theorem prov ing. J.ACM 12,4 (1965), 536-541.