Journal of the Association for Computing Machinery, Vol. 40, No. 3, July 1993, pp. 504–535.

Dissolution: Making Paths Vanish

NEIL V. MURRAY

AND

ERIK ROSENTHAL

Abstract. Path dissolution, a rule of inference that operates on formulas in negation normal form and that employs a representation called semantic graphs, is introduced. Path dissolution has several advantages in comparison with many other inference technologies. In the ground case it preserves equivalence and is strongly complete: Any sequence of dissolution steps applied exhaustively to a semantic graph G will yield an equivalent linkless graph G′. Furthermore, one need not (and cannot) restrict attention to conjunctive normal form (CNF) when employing dissolution: A single application (even to a CNF formula) generally produces a non-CNF formula that is more compact than any of its CNF equivalents.

Path dissolution is a global rule; as such, it is employed at the first order level differently from the way locally-oriented techniques such as resolution are. Two methods for employing dissolution as an inference mechanism for first order logic are presented.

Dissolution is briefly related to the author’s theory links mechanism, the factoring of formulas with the distributive laws, and to analytic tableaux. Some preliminary experimental results are also reported.

Categories and Subject Descriptors. F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic—computational logic; mechanical theorem proving; G.2.2 [Discrete Mathematics]: Graph Theory; I.2.3 [Artificial Intelligence]: Deduction and Theorem Proving—deduction; metatheory; resolution

General Terms. Algorithms, Theory

Additional Key words and Phrases. Automated deduction, inference, matrix methods, path, Prawitz analysis

Copyright 1993 by ACM, Inc. Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from Publications Dept, ACM Inc., fax +1 (212) 869-0481, or permissions@acm.org.