---
title: "Universal Unification and Regular Equational ACFM Theories"
authors:
  - "Jörg H. Siekmann"
  - "Peter Szabó"
doi: ""
url: "https://ijcai.org/proceedings/1981/100"
pdf: "https://ijcai.org/proceedings/1981/0100.pdf"
venue: "Proceedings of the Seventh International Joint Conference on Artificial Intelligence"
year: 1981
pages: "532-537"
track: "Theorem Proving"
keywords:
---

# Universal Unification and Regular Equational ACFM Theories

Jörg H. Siekmann, Peter Szabó

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