And-Or Graphs Applied to RUE Resolution

1. INTRODUCTION

In resolution b unification and e ualit (RUE resolution , we augment the standard theory of binary resolution due to [Robinson,l965] by the notion of disagreement sets, to incorporate the axioms of equality into the definition of resolution and eliminate the use of these axioms in refutations.

In RUE resolution we resolve to inequalities when the mgu does not exist; for example, the E-unsatisfiable set:

is refuted by:

Acknowledgement: Subrahmanian supported by USAF Grant FJ0602-85-C-0008.

James J. Lu, V. s. Subrahmanian Dept. of Computer Science Syracuse University Syracuse, New York 13210

RUE refutations are succinct and typically less than half as long as corresponding refutations with the equality axioms. Furthermore, RUE resolution is complete without using paramodulation or the equality axioms. Experiments with a theorem prover based on this method have produced superior results which are described in [Digricoli and Harrison,l986].

2. RUE Resolution

The basic definitions underlying RUE resolution are the following:

A Disagreement Set of a Pair of Terms:

"If s,t are non-identical terms, the set of one element, a pair, [s:t}, is the origin disagreement set. If s,t have the form: f(a 1 , ··· ,ak),f(b 1 , ··· ,bk)' then the set of pairs of corresponding arguments that are not identical is the to~most disa~eement set. Furthermore, 1f D is a isagreement set, then (D - [e}) U D is also a disagreement set, where e eis an element of D and De is a disagreement set of e,"

For example:

A Disagreement Set of Complementary L1terals:

"A disagreement set of complementary literals, P( s 1 , ··· , sn), P( t 1 , ··· , tn), is defined as the union:

where D. is a disagreement set of the l corresponding arguments, si,ti ·

The topmost disagreement set of P(s 1 , ... ,sn)' P(t 1 , ... ,tn) is the set of pairs of corresponding arguments that are not identical. Applying the substitution axiom for predicates, we can state that:

where D now represents a disjunction of inequalities specified by any disagreement set of P,not P. In resolution by unifi­ cation and equality we can resolve P and P immediately to D. For example, we may resolve:

in four distinct ways dependent on our choice of disagreement set; namely to any one of the following resolvents:

It is in fact, the second resolvent which is required to refute S in the previous example. Hence, RUE resolution requires a decision mechanism to select the approp­ riate disagreement in resolving comple­ mentary literals. Furthermore, we show in [Digricoli and Harrison,l986] that the substitution to be applied before resolv­ ing in a refutation may be neither the mgu (when it exists) nor the mgpu, the most general partial unifier, a relaxed form of the mgu which permits us to pass over irreducible disagreements. Instead we define the RUE unifier as the appropriate substitution.

In the theory of RUE resolution in strong form, both the decision mechanism to select disagreement sets and the definition of the RUE unifier depend on a viability test defined as follows:

"A Disagreement Set D is Viable in respect to a set of clauses S only if:

for each s.lt. corresponding to D, l l we have that for si there is a term ~ which is the argument of a positive equality literal inS such that s. either unifies with a or matches 1 a on leading function symbol. In the latter case, s.:a must have a viable disagreement set below the origin disagreement, Similarly for ti and some other term b which is the argument of a positive equality literal inS."

For example, in respect to:

the complementary literals, P and P, have only one viable resolvent:

ale is viable since both a and c unify with arguments of equality literals inS. g(b)lg(d) is viable since g(b) matches on function symbol with g(c) in clause 5 (with b:c being viable), Furthermore, g(d) unifies with g(d) in the same clause. Hence, the entire resolvent is viable and leads to the refutation already stated,

Notice , however, that: ale v bid is not viable as a resolvent of P,P, since the inequality bid is not viable since d does not unify with the argument of an equality literal ins. Furthermore, f(a)lf(c) v g(b)lg(d) is not viable since f(a)lf(c) is not viable.

Byviable we mean "can possibly ;participate in a refutation". In LDigricoli and Harrison,l986] we prove that if an inequality is not viable, it either cannot participate in a refutation of S or must be reduced to a lower disagreement . We also state that the definition of viability is recursi~and the recursive iteration is finite, since each of the terms s. and t. has a finite nesting of function 1 symbol~. The recur­ sion peels these off and thus terminates,

It is precisely here that the definition of viability is flawed since the last statement is not true. Lu and Subrahmanian [1988] point out counter examples which show that a non-terminating iteration can occur in applying the viability test. The following clause set, for example, leads to non-terminating iteration:

P and P can only resolve to f(a,b)ld, but this inequality when tested for viability leads to a non-terminating iteration: f(a ,b) matches on function symbol with f(f(a,b),c) and we must test alf(a,b) and blc for viability, But the first inequality reintroduces f(a,b) which again must be matched with f(f(a,b),c), ad infinitum.

Since in RUE theory, the concept of viability plays a central role in defining the RUE unifier and the topmost viable disagreement set, the possibility of non­ termination undermines the theory of RUE resolution in strong form unless we can show how to avoid non-termination. The primary subject of this paper is to show how the theory of And-Or graphs due to [Chang and Slagle,l971] can be used to solve this problem.

J, The Theory of And-Or Graphs

A node in an _A..."1d-Or __ g£aph:... r~pres:enits. a problem to be solved. We define an And-expansion:

as denoting that problem p is solved if the logical And of subprob£ems p 1 ,p 2 , ·· ,p is solved, i.e., we decompose p in to n subproblems p 1 ,p 2 , ·.· ,p, all o~ which must be solvea in ordernto solve p 0 ·

Similarly we define an Or expansion:

to denote that p is solved if any one of the subproblems 0 p 1 ,p 2 , ·.. ,pn is saved.

Mixed expansions are permitted so that:

denotes that p 0 becomes (p 1 A p 2 ) v p 3 ·

In an And-Or graph we repeatedly perform decomposition until we reach primitive subproblems which are known to be solvable or unsolvable. These are the leaf nodes of the graph. The entire graph represents a system of boolean substitu­ tions for the root node,

A set of lea:fl :node.s, 'the .. so1uti'on '.o.f all of which implies the solution of the root node, is called an implicant of the root. One implicant is said to subsume another implicant if it is a subset of that implicant. For example, if we denote nodes by numeric indices, then [?,8} subsumes [2,?,8,9} and, furthermore, since [?,8} is a simpler solution, we should discard [2,?,8,9}. Subsumption will play an important role in our work.

The situation becomes interesting because of circularity. The And-Or graph:

has no solution due to circularity. But the cyclic And-Or graph:

has one solution: p 4 A p? ·

An And-Or graph with many nodes and cycles may represent a very complex problem decomposition. The following algorithm stated by Chang and Slagle will compute the implicants of an arbitrary And-Or graph:

Implicant Algorithm:

l. Initialize the current formula to the root node,

2. Select any non-leaf node in the current formula (for example, the lowest numbered node) and substitute its boolean expansion as stated in the And-Or graph, for each occurrence of this node in the current formula.

), Remove from the current formula any implicant which is subsumed by another implicant in the current formula or by an implicant which previously appeared in the current formula.

4. Repeat steps (2) and (3) until the current formula either vanishes (there is no solution for the root due to cycles in the graph) or only leaf nodes appear in the current formula. In the latter case, the final state of the current formula, when no further substitutions are possible, represents a disjunction of the alternative implicants of the And-Or graph.

For example consider the And-Or graph taken from LNilsson,l971, p.l26]

The algorithm converges to five distinct implicants and subsurnption was used to filter out the effect of the cycle in the graph.

Chang and Slagle prove that their a l gorithm always converges to solution implicants or to the empty formula, i rrespective of cycles in the graph. Nilsson who gives a good treatment of And-Or graphs in [1971] fails to mention t he implicant algorithm which seems to be absent from most texts in artificial i ntelligence.

4 . And-Or Graphs Applied to Viability

Conside~ our previous clause set:

Can S be refuted? The only possible r esolution is:

so the question arises: is this inequality viable? We have previously shown that the viability test does not terminate when applied to this inequality. In point of f act, this inequality is not viable since we cannot deduce f(a,b)=d from S.

If we state the recursive application of the viability test as an And-Or graph, we can show that f(a,b)ld is not viable because the And-Or graph for viability has no solution, the implicant algorithm converges to the empty formula:

In the above, a(J), b(4), c(4) and d(5), denote the clause numbers in which unification occurs. We apply the implicant algorithm to the above:

The reader should review the defini­ tion of viability and then follow the decomposition that occurs in the And-Or graph which simply traces the recursive application of the viability test. The And-Or graph contains no duplicate nodes; hence, in expanding node 4 we cycle back to node 2, creating a cyclic graph. All the circularity which occurs during the viability test will produce cycles in the And-Or graph which are analyzed by the implicant algorithm to determine viability.

We impose the condition that the nodes of a viability graph be mutually distinct so that if a successor node already exists in the graph we arc back to that unique representation in the graph. The leaf nodes of a viability graph will necessarily be either unsolvable argument nodes (the viability test is not satisfied) or solved unification nodes (a term unifies with the argument of an equality literal). The root inequality is viable if and only if the implicant algorithm converges to at least one implicant composed purely of solved unification nodes. In RUE resolu­ tion in strong form we are required to resolve to the topmo~t viable disagree­ ment set (each inequality must be viable and nearest the topmost disagreement of the complementary literals resolved.

The And-Or graph for the viability of an inequality will always be finite since the number of distinct terms or subterms inS is finite and duplicate nodes are not permitted in the graph.

We will present the strict formaliza­ tion of the concept of an And-Or graph applied to viability, defining the differ­ ent types of nodes present in the graph, namely, inequality nodes, argument nodes, unification nodes, function-matching nodes and disagreement set nodes, in a proximate future paper.