Combination of Unification Algorithms in Equational Theories

Abstract

Unification in equational theories, i.e., solving equations in varieties, is a basic operation in Artificial Intelligence, in Computer Science and in particular in the field of Automated Deduction. A shortcoming of most known unification algorithm is that they are usually designed for a restricted set of terms only. A method is presented to combine unification algorithms for special equational theories (with disjoint sets of function symbols) to overcome this drawback. This method applies to regular and collapse-free equational theories (a theory is regular if all its axioms have the same variables on each side and it is collapse free if it does not contain an axiom of the form x = t, where x is a variable and t is a non-variable term). The basic idea is first to replace certain subterms by constants and then to unify these constant abstractions. In a recursive step the replaced subterms are considered in turn. Provided the constituent theories are finitary (a finite minimal complete set of unifiers always exists) the combination algorithm is shown to be totally correct. The termination proof is based on an idea of Fages’ termination proof for Stickel’s associative and commutative unification algorithm. The abstract algorithm is applied to the theory of associativity and commutativity thus extending the algorithm of Livesey and Siekmann to the whole class of first order terms. As a second example of application the theory of commutativity is discussed. In order to investigate the limitations of the approach above, the theory of idempotence, which is a collapse theory, is studied and a new idempotent unification algorithm for the class of first order terms is presented.

Unifikation in Gleichheitstheorien, d.h. Lösen von Gleichungen in Varietäten, ist eine grundlegende Operation in der Künstlichen Intelligenz, in der Informatik und insbesondere im Automatischen Beweisen. Ein Nachteil beim Einsatz fast aller bekannten Theorieunifikationsalgorithmen ist die Tatsache, daß diese nur für eine eingeschränkte Teilklasse von Termen konzipiert worden sind. Es wird eine Methode vorgestellt, die Unifikationsalgorithmen verschiedener spezieller Gleichheitstheorien kombiniert, um die obigen Unzulänglichkeiten zu überwinden. Die Methode ist für reguläre und kollapsfreie Gleichheitstheorien mit paarweise disjunkte Mengen von Funktionssymbolen anwendbar (eine Theorie ist regulär, falls ihre Axiome dieselben Variablen auf beiden Seiten enthalten, und kollapsfrei, wenn sie keine Axiome der Form x = t enthält, wobei x eine Variable und t ein nichtvariabler Term ist ). Die Kernidee des Algorithmus ist es, gewisse Unterterme durch Konstanten zu ersetzen, die so abstrahierten Ausgangsterme zu unifizieren und dann die ersetzten Terme analog zu behandeln. Für den Fall, daß die Teiltheorien finitär sind (d.h. es existiert immer eine endliche minimale vollständige Menge von Unifikatoren), wird die totale Korrektheit des Algorithmus gezeigt. Der Terminierungsbeweis baut auf einer Idee von Fages auf, mit Hilfe derer er die Terminierung von Stickels Unifikationsalgorithmus für Assoziativität und Kommutativität gezeigt hat. Der abstrakte Algorithmus wird nun auf die Theorie der Assoziativiät und Kommutativität angewendet und man erhält so eine Erweiterung des Livesey und Siekmannschen Algorithmus auf die volle Klasse der Terme erster Ordnung. Als zweites Anwendungsbeispiel wird die Theorie der Kommutativität diskutiert. Um die Grenzen des Ansatzes zu studieren, wird exemplarisch die Theorie der Idempotenz, eine Kollapstheorie, untersucht. Daraus entsteht ein neuer Unifikationsalgorithmus für Terme erster Ordnung, die idempotente Funktionssymbole enthalten.