AbstractWe introduce a graphical representation of quantifier-free predicate calculus formulas in negation normal form and a new rule of inference that employs this representation. The new rule, path resolution, is an amalgamation of resolution and Prawitz analysis. Our goal in the design of path resolution is to retain some of the advantages of both Prawitz analysis and resolution methods, and yet to avoid to some extent their disadvantages.
Path resolution allows Prawitz analysis of an arbitrary subgraph of the graph representing a formula. If such a subgraph is not large enough to demonstrate a contradiction, a path resolvent of the subgraph may be generated with respect to the entire graph. This generalizes the notions of large inference present in hyper-resolution, clash-resolution, NC-resolution, and UR-resolution.
A class of subgraphs is described for which deletion of some of the links resolved upon preserves the spanning property. Copyright 1987 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
Additional Key Words and Phrases: Automated deduction, connection graph, inference, link deletion, path, Prawitz analysis
Selected papers that cite this one
- Neil V. Murray and Erik Rosenthal. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504-535, July 1993.