The Efficacy of RUE Resolution Experimental Results and Heuristic Theory
Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 539-546.
Abstract
We present and analyze experimental results in the first extensive use of a theorem prover based on Resolution by Unification and Equality. Implicit use is made of equality axioms by the inference rules RUE and NRF to achieve incisive refutations for E-unsatisfiability. Since a primary issue in automated deduction is the efficacy of convergence to proof, we describe in detail the heuristics which were used to obtain proofs. A comparative tabulation with the results of McCharen, Overbeek and Wos, who used unification resolution, shows sharply reduced cumulative unification counts.
@inproceedings{ijcai1981p101,
title = {The Efficacy of RUE Resolution Experimental Results and Heuristic Theory},
author = {Digricoli, Vincent J.},
booktitle = {Proceedings of the Seventh International Joint Conference on
Artificial Intelligence, {IJCAI-81}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Roger C. Schank},
pages = {539--546},
year = {1981},
month = {8},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1981/101},
}
TY - CPAPER TI - The Efficacy of RUE Resolution Experimental Results and Heuristic Theory AU - Digricoli, Vincent J. T2 - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81 PB - International Joint Conferences on Artificial Intelligence PY - 1981 SP - 539 EP - 546 UR - https://ijcai.org/proceedings/1981/101 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
