The goal of this project is to develop a general purpose portable system for automated reasoning based on a new inference rule - RUE Resolution - which incorporates the axioms of the equality into the definition of resolution, producing much shorter and more transparent proofs. Experiments with a prototype RUE theorem prover have produced excellent comparative results. A theoretical study of the implications of RUE resolution as applied to Logic Programming, to the Reduction Method of Knuth and to Paramodulation will be made.
