Path Resolution with Link Deletion
Proceedings of the Ninth International Joint Conference on Artificial Intelligence. Theorem Proving. 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 .
@inproceedings{ijcai1985p241,
title = {Path Resolution with Link Deletion},
author = {Murray, Neil V. and Rosenthal, Erik},
booktitle = {Proceedings of the Ninth International Joint Conference on
Artificial Intelligence, {IJCAI-85}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Aravind Joshi},
pages = {1187--1192},
year = {1985},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1985/241},
}
TY - CPAPER TI - Path Resolution with Link Deletion AU - Murray, Neil V. AU - Rosenthal, Erik T2 - Proceedings of the Ninth International Joint Conference on Artificial Intelligence, IJCAI-85 PB - International Joint Conferences on Artificial Intelligence PY - 1985 SP - 1187 EP - 1192 UR - https://ijcai.org/proceedings/1985/241 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
