---
title: "E-Resolution: Extension of Resolution to Include the Equality Relation"
authors:
  - "James B. Morris"
doi: ""
url: "https://ijcai.org/proceedings/1969/28"
pdf: "https://ijcai.org/proceedings/1969/0028.pdf"
venue: "Proceedings of the First International Joint Conference on Artificial Intelligence"
year: 1969
pages: "287-294"
track: "Theorem Proving"
keywords:
---

# E-Resolution: Extension of Resolution to Include the Equality Relation

James B. Morris

*Proceedings of the First International Joint Conference on Artificial Intelligence*, pages 287-294.

## Abstract

The E-Resolution inference principle described in this paper is a single-inference logic system for the first-order predicate calculus with equality. Special axioms for equality (i.e., axioms for symmetry, reflexivity, transitivity, and substitutivity) are not required to be added to the original set of clauses. Other advantages of E-Resolution are the relatively small number of intermediate clauses which must be retained in a proof and the distinct possibility that search strategies suitable for Resolution will also be suitable for EResolution. Although it is not known whether or not E-Resolution is complete, this topic is currently being investigated by the author. Key terms: automatic theorem-proving, equality substitution, E-Resolution, firstorder predicate calculus with equality, theorem-proving.