AbstractPath 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. Copyright 1993 by ACM, Inc.
The abstract is also available as a LaTeX file, a DVI file, or a PostScript file.
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
Selected papers that cite this one
- Bernhard Beckert, Reiner Hähnle, and Gonzalo Escalada-Imaz. Simplification of many-valued logic formulas using anti-links. Journal of Logic and Computation, 8(4):569-587, August 1998.
- Reiner Hähnle and Stefan Klingenbeck. A-ordered tableaux. Journal of Logic and Computation, 6(6):819-833, December 1996.
Selected references
- Peter B. Andrews. Theorem proving via general mappings. Journal of the ACM, 28(2):193-214, April 1981.
- Wolfgang Bibel. On matrices with connections. Journal of the ACM, 28(4):633-645, October 1981.
- Stephen Cook and Robert Reckhow. On the lengths of proofs in the propositional calculus (preliminary version). In Conference Record of Sixth Annual ACM Symposium on Theory of Computing, pages 135-148, Seattle, Washington, 30 April-2 May 1974.
- Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, July 1960.
- Neil V. Murray and Erik Rosenthal. Inference with path resolution and semantic graphs. Journal of the ACM, 34(2):225-254, April 1987.