Path Resolution with Link Deletion
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 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 iu hyperresolution, clash-resolution, NC-resolution, and PLresolution. Two forms of path resolution are described for which deletion of the links resolved upon preserves the spanning property. 1.
Cite
Text
Murray and Rosenthal. "Path Resolution with Link Deletion." International Joint Conference on Artificial Intelligence, 1985.Markdown
[Murray and Rosenthal. "Path Resolution with Link Deletion." International Joint Conference on Artificial Intelligence, 1985.](https://mlanthology.org/ijcai/1985/murray1985ijcai-path/)BibTeX
@inproceedings{murray1985ijcai-path,
title = {{Path Resolution with Link Deletion}},
author = {Murray, Neil V. and Rosenthal, Erik},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1985},
pages = {1187-1193},
url = {https://mlanthology.org/ijcai/1985/murray1985ijcai-path/}
}