---
title: "The Efficacy of RUE Resolution Experimental Results and Heuristic Theory"
authors:
  - "Vincent J. Digricoli"
doi: ""
url: "https://ijcai.org/proceedings/1981/101"
pdf: "https://ijcai.org/proceedings/1981/0101.pdf"
venue: "Proceedings of the Seventh International Joint Conference on Artificial Intelligence"
year: 1981
pages: "539-546"
track: "Theorem Proving"
keywords:
---

# The Efficacy of RUE Resolution Experimental Results and Heuristic Theory

Vincent J. Digricoli

*Proceedings of the Seventh International Joint Conference on Artificial Intelligence*, 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.