Equality Reasoning in Clause Graphics

1. INTEGRATION OF PATHS INTO THE PROOF PROCEDURE

Just like R-links and P-links paths should also be searched for and created at the beginning, when the initial graph is formed, this information should then be inherited during the subsequent search for a proof.

But because of the undecidability of equality of two t e rms not all the necessary ER-paths can be found in the initial graph. For that reason a new link type, PER-link (potential E-resolution link) connecting potentially complementary unifiable literals is introduced into the graph. These PER­ links provide the top-level information for the proof procedure to search for the corresponding ER-paths, and during this search three cases can occur:

1. All possible ER-paths corresponding to a PER-link are found.
2. It is detected that no ER-path for a given PER­ link exists.
3. The search for ER-paths is stopped because of space or time limitation.

For each of these cases differ ent operations are performed:

1. If all ER-paths are found, then the PER-link is replaced by the ER-paths. All possible ways to r emove the differences between the literals of the PER-link are known and given by the ER-paths. If an ER-path is selected in the proof, then the E-resolution corresponding t o the ER-path is executed.
2. Ther e exists no ER-path between the literals of the PER-link, i.e. the differences of the respec­ tive terms cannot be r emoved completely and therefore the PER-link is del eted.
3. If the search is stopped and no (or not all) ER-paths are found, then the PER-link remains in the graph. If a PER-link is selected, then an operation to reduce the differences between the literals of the PER-link i s executed using the information obtained from the incomplete search.

PER-links are treated as a special case and are only used in global strategies as auxiliary links which control the search for paths and enable sen­ sible operations to r educe differences of potential­ ly complementary unifiable literals as compensation for the lacking ER-paths (case c above) .

During the search for a proof ER-paths as well as PER-links are inherited and used to compute new ER-paths and new PER-links. Hence each ER-path used in the proof was already present in the initial graph or has been inherited from an initial ER-path.

This method of using ER-paths has three main advan­ tages:

• (i) ER-paths and PER-links contain important information for global strategies which plan and control the whole search for a proof (see [BESSHW81], (SS81 ], [Oh82 ]). This information is particularly useful because it is already available at the beginning of the proof.
• (ii) An efficient handling of equality is possible, because the search is done in the small ini­ tial graph only. Furthermore only a few paths have to be searched for; most paths are found by inheritance.
• (iii) Strong additional deletion rules are available which greatly reduce the potential number of paths as well as the size of the graph . For example in case b) above the deletion of a PER-link may lead to a pure clause just as for the usual clause graph proof procedure,

thus causing the we ll-known snowball effect of deletions to start.

2. THE SEARCH FOR PATHS USING CONSTRAINTS

An unsophisticated and exhaustive search for ER-paths is prohibitively expensive because of the very large search space. The size of this essentially depends on the number of equations (ne) in the c lause set, on the average number of subterms (ns) in a literal, and on the ratio (r) of positive to total unifica­ tion tests for possible equality r eplacements. Finally it also depends on the search depth (sd). A breadth first search procedure, like that of Morris [Mo69 ) must execute ( (2 * ne * ns * r) sd *1 /r) calls of the unification a lgorithm. Also it has to

carry out (2 * ne * ns * r)sd equality r eplacements in order to get all possible E-resolvents for ~ PER-link. For example, if a c lause set has ten equations, an average of five subterms per literal and a unification success rate of 10%, the n a search

depth of t en steps requires 10 11 calls of the unification algorithm and 10 10 replacement operations. To make the situation worse Morris [Mo69 ) observed that in usual clause sets f o r most PER-links the re does not exist an E-resolvent, but since the search must be done completely most of the effort is spent in vain.

In order to obtain a practicable search procedure the enormous sear c h space has t o be reduced. In the following we propose a r eduction of the search space by exploiting constraints. The constraints use the information contained in the P-links.

For a clause graph <S> and a PER-link there are usually many P-links connecting the effective equa­ tions and the two literals . If these P-links are visualized graphically, certain structures emerge, e .g . an equality-chain in the simple example 1. But in most cases the structure is a more complex equa­ lity-net as example 2 demonstrates:

Example 2

An equality-net (EN) and the compatibility of an equality-net are defined in [Bl83] as a special graph structure of P-links. Each compatible equality­ net builds an ER-path and represents a possible E-resolution step. Conversely there exists for each possible E-resolution a compatible EN in the graph which builds the appropriate ER-path. These condi­ tions are ensured because the PeG-Procedure is complete [SW79 ). In order to find the ER-paths the compatible equality-nets must now be searched for.

To this end several conditions can be stated which are necessary but not sufficient f o r the compatibi ­ lity of an EN. Such constraints are checked step by step the reby drastically r educing the search space.

Two examples will show possible r easons for the in­ compatibility of equality-ne ts.

Exampl e 4

In Example 3 the combination of the P-links 1 and 2 is imposs ible because their unifiers [x + a) and [x + b) are incompatibl e . . In example 4 the P-links 1 and 2 are incompatible, because after paramodula­ tion on link 1, link 2 cannot be inherited t o the paramodulant < Pb > since the access depth does not coincide .

Some of the constraints to be used are:

1. In a compatible EN all unifie rs of the p-links concerned must merge to one mgu (i.e. the uni­ fi ers must be compatible, provided a proper variable r enaming has been carried out) .
2. 2 ) In a compatible EN : for each maximal equality­ chain in the EN the s um of all access depths must be equal to z e r o and each partia l sum must be l ess than or equal to zero.
3. In a compatible EN, no chain of two links in the EN is incompatible, i.e. if an equality-chain of length 2 is incompatible, then each EN which contains this equality-chain i s also incompatib - le. (Note: incompatible is defined in [ Bl83 ) and is diffe rent from not compatibl e .)

The searc h procedure can be improved by introducing additional constraints.

Although suc h constraints are powerful it is not expensive to test them, for exampl e only some inte ­ ge rs must be added to detect the incompatibility of an EN caused by condition 2.

After reduction of the search space the most promi­ sing ENs are selected for a _full compatibility test and the surviving candidates are used to build the ER-paths.

The method outlined here of handling equality is described in [Bl83) whe re the formal notions are developed and additional results are presented. This me thod is presently b e ing impleme nte d and evaluated as part of the Markgraf Karl Refutation Procedure [BESSHW81), [Oh82).

LITERATUR

[sS81]

[An70 ]

R. Anderson: Completeness results for E-Resolution. Proc. Spring Joint Conf., 1970,653-656

[BESSHW81] K.H. Blasius, N. Eisinger, J. Siekmann, G. Smolka, A. Herold, C. Walther: The Markgraf Karl Refutation Procedure. Proc. IJCAI, 1981, 511-518

[Bl 83 )

K.H. Blasius: Equality-Reasoning in clause graphs. Universitat Karlsruhe, Interner Bericht (to appear)

[Br75 ] D. Brand: Proving Theorems with the Modification Me thod. SIAM Journal of Comp., vol 4, no. 4, 1975

(Di79 ) V.J. Digricoli: Resolution by Unification and Equality. Proc. 4th Workshop on Automated Deduction, 1979, Texas

(HR78) M.C. Harrison, N. Rubin: Another Generalization of Resolution. JACM, vol 25, no. 3, July 1978

[Ko75 ] R. Kowalski: A Proof Procedure Using Connection Graphs.

JACM 22, 4, 1975

[Lo78] D. Loveland: Automated Theorem Proving: A logical Basis. North Holland, 1978

[Mo69] J.B. Morris: E-Re solution: An Extension of Resolution to include the Equality Relation.

Proc. IJCAI, 1969, 287-294

[Oh82) H.J. Ohlbach: The Markgraf Karl Refutation Procedure, the Logic Engine. Universitat Karlsruhe, Interner Bericht,

1982

(RW69) G. Robinson, L . Wos: Paramodulation and TP in first order theories with equality.

Machine Intelligence 4, 135-150

[Sh78 ] R.E. Shostak: An Algorithm for Reasoning About Equality. CACM, July 1978, vol 21, no. 7

E.E. Sibert: A machine-oriented Logic incorporating the Equality Axiom. Machine Intelligence, vol 4, 1969,

[Si69) 103-133

(SW79)

J. Siekmann, G. Smolka: Selection Heuristics, Deletion Strategies and N-Level Terminator Configurations for the Connection Graph Proof Procedure. Universitat Karlsruhe, Research Report, 1981

J. Siekmann, G. Wrightson: Paramodulated Connectiongraphs. Acta Informatica, 1979