Universal Unification and Regular Equational ACFM Theories
Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theorem Proving. Pages 532-537.
Abstract
A universal minimal type conformal matchlng algorithm and a universal minimal unification algorithm based on [FA79J, [SL74J, [LB79J, [HUBOJ are presented for a restricted class of equational theories (the Regular ACFM Theories), i.e. it is shown that the set of most general unifiers is recursively enumerable for this class. The class of Regular ACFM Theories is wide enough to containmost special cases of unification algorithms that have been investigated so far. This paper is a (very) abbreviated version of [SS81cJ, all proofs and most of the technical material are omitted for lack of space . For reasons of consistency with the original paper, the numbering of definitions, lemmas and theorems has been retained.
@inproceedings{ijcai1981p100,
title = {Universal Unification and Regular Equational ACFM Theories},
author = {Siekmann, Jörg H. and Szabó, Peter},
booktitle = {Proceedings of the Seventh International Joint Conference on
Artificial Intelligence, {IJCAI-81}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Roger C. Schank},
pages = {532--537},
year = {1981},
month = {8},
note = {Theorem Proving},
url = {https://ijcai.org/proceedings/1981/100},
}
TY - CPAPER TI - Universal Unification and Regular Equational ACFM Theories AU - Siekmann, Jörg H. AU - Szabó, Peter T2 - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81 PB - International Joint Conferences on Artificial Intelligence PY - 1981 SP - 532 EP - 537 UR - https://ijcai.org/proceedings/1981/100 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
