Path resolution and semantic graphs

Abstract

We introduce a new rule of inference, path resolution, which operates on a graphical representation of quantifier-free predicate calculus formulas. 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. The main advantage of Prawitz analysis is that, except for variants of original formulas, no new formulas are inferred which rapidly expand the search space. However, except for adding variants, Prawitz analysis is an all or nothing time-bound search for a contradiction. In contrast, resolution and other inference based methods store the progress made at each inference by retaining the inferred formula. Eventually localized evidence of a contradiction is produced, for example the empty clause. The required multiple variants of formulas are automatically (and often excessively) generated. But each new formula introduced interacts with others, expanding the search rapidly in both time and space. One of the disadvantages of resolution is its reliance on conjunctive normal form. We avoid conjunctive and disjunctive normal form and the duplication of literals that their use may necessitate, since path resolution operates on formulas in negation normal form. We have found that the analysis is greatly simplified by a representation of NNF formulas which we call ‘semantic graphs.’ Path resolution allows Prawitz analysis of an arbitrary subgraph of the existing graphical representation of formulas. 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 UL-resolution.