---
title: "Path Resolution with Link Deletion"
authors:
  - "Neil V. Murray"
  - "Erik Rosenthal"
doi: ""
url: "https://ijcai.org/proceedings/1985/241"
pdf: "https://ijcai.org/proceedings/1985/0241.pdf"
venue: "Proceedings of the Ninth International Joint Conference on Artificial Intelligence"
year: 1985
pages: "1187-1192"
track: "Theorem Proving"
keywords:
---

# Path Resolution with Link Deletion

Neil V. Murray, Erik Rosenthal

*Proceedings of the Ninth International Joint Conference on Artificial Intelligence*, pages 1187-1192.

## Abstract

We introduce a graphical representation of quantifier-free predicate calculus formulas and a new rule of inference which employs this representation . The new rule is an amalgamation of resolution and Prawitz analysis which we call path resolution. Path resolution allows Prawitz analysis of an arbitrary subgraph of the graph representing a formula. If such a subgraph is not !arge enough to demoostrate a contradiction, a path resolvent of the subgraph may be generated with respect to the entire graph. This generalizes the notions of !arge inference present in hyperresolution, clash-resolution, NC-resolution, and ULresolution. Two forms of path resolution are described for which deletion of the links resolved upon preserves the spanning propcrty .