E-Resolution: Extension of Resolution to Include the Equality Relation
Proceedings of the First International Joint Conference on Artificial Intelligence. Theorem Proving. 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.
@inproceedings{ijcai1969p28,
title = {E-Resolution: Extension of Resolution to Include the Equality Relation},
author = {Morris, James B.},
booktitle = {Proceedings of the First International Joint Conference on
Artificial Intelligence, {IJCAI-69}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Donald E. Walker and David C. Cooper},
pages = {287--294},
year = {1969},
month = {5},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1969/28},
}
TY - CPAPER TI - E-Resolution: Extension of Resolution to Include the Equality Relation AU - Morris, James B. T2 - Proceedings of the First International Joint Conference on Artificial Intelligence, IJCAI-69 PB - International Joint Conferences on Artificial Intelligence PY - 1969 SP - 287 EP - 294 UR - https://ijcai.org/proceedings/1969/28 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
