The efficacy of rue resolution experimental results and heuristic theory
Vincent J. Digrigoli · International Joint Conference on Artificial Intelligence · 1981
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.