Journal of the Association for Computing Machinery, Vol. 34, No. 2, April 1987, pp. 225–254.

Inference with Path Resolution and Semantic Graphs

NEIL V. MURRAY

AND

ERIK ROSENTHAL

Abstract. We 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, NCresolution, and UR-resolution.

A class of subgraphs is described for which deletion of some of the links resolved upon preserves the spanning property.

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

Copyright 1987 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.