The Efficacy of RUE Resolution Experimental Results and Heuristic Theory
Abstract
We present and analyse 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 efficiancy 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.
Cite
Text
Digricoli. "The Efficacy of RUE Resolution Experimental Results and Heuristic Theory." International Joint Conference on Artificial Intelligence, 1981.Markdown
[Digricoli. "The Efficacy of RUE Resolution Experimental Results and Heuristic Theory." International Joint Conference on Artificial Intelligence, 1981.](https://mlanthology.org/ijcai/1981/digricoli1981ijcai-efficacy/)BibTeX
@inproceedings{digricoli1981ijcai-efficacy,
title = {{The Efficacy of RUE Resolution Experimental Results and Heuristic Theory}},
author = {Digricoli, Vincent J.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1981},
pages = {539-547},
url = {https://mlanthology.org/ijcai/1981/digricoli1981ijcai-efficacy/}
}