Unification is a well established concept in artificial intelligence and automated theorem proving, in computational linguistics and universal algebra as well as in theoretical and applied computer science like for example in the semantics of programming languages, for the semantic web and in many other areas (see [50, 65, 76] for several application areas). Surveys of unification theory can be found in [7, 8, 31, 50, 76] and there is more recent work on unification in description logics [4, 10, 11], modal logics [5], nominal unification [81], disunification [9] and other application areas. The current state of the art is represented at the UNIF workshop series.[1] A survey of the related topic of rewriting systems is presented in [22] and in the “emerging” textbook [48]; a list of open problems can be found in [68]. A standard textbook is by Franz Baader and Tobias Nipkow, Term Rewriting and All That [6]. An interesting collection of open and solved unification problems for several common algebraic structures like groups, vector spaces, commutative rings, Boolean algebras and others is collected by Stanley Burris and a recent survey on higher order unification is presented in [41].

Unification algorithms were first invented for automated theorem proving systems and the historically first computer generated mathematical proof for a theorem was found by a program from Martin Davis in 1954. It postulated the remarkable fact that the product of two even numbers is again even, formulated in a decidable fragment of first order logic, called Pressburger Arithmetic. The first complete unification algorithm for first order logic is due to Prawitz [64], but a complete algorithm as


we know it today was working already in 1963 in Martin Davis’s “Davis-Putnam Procedure” [20], where improvements were implemented by D. McIlroy and Peter Hinman. All of this, including Martin’s linked conjunct method, was later subsumed by Alan J. Robinson’s resolution principle [67], where the unification algorithm is the corner stone of this method. Resolution dominated the field of automated reasoning then for many decades to come and is still the most wellknown inference rule in artificial intelligence.

Unification as we see it today is a general mechanism to solve equational problems. For practical applications it is often crucial to have a minimal representation of the solutions, from which all other solutions (unifiers) can be derived. This is an essential feature of any of todays resolution, matrix, rewrite or tableaux based automated reasoning systems, where the most general unifier represents the infinitely many elements from the Herbrand Universe that had to be enumerated and instantiated into the universally quantified variables of earlier automated deduction systems. All of these early sytems implemented the key idea of Herbrands work [84], that a first order formula can be proven by instantiating in a systematic fashion the quantified universal variables by ground terms, (now often called the Herbrand Universe)3 and then prove it by some decision procedure for propositional logic. These early systems like Gilmore [33], Wang [83], Kangar [45], Davis [20], Veenker [82] and others differed in their struggle to find the “right” instances out of the infinite set of potential ground terms and it took a little more than a decade until the notion of a complete first order unification algorithm became standard. Martin Davis’s article “The prehistory and early history of automated deduction” [17] gives a lively historical account of these early developments and the two volumes [78] collect the most important contributions in these early days.

Martin also worked with Julia Robinson on Hilbert’s Tenth Problem [18], a topic we shall pick up again in paragraph 4.2 where we discuss its relationship to string unification. For all these well known and influential contributions and many more personal reasons this article is dedicated to Martin Davis.

For unification problems in the free algebra of terms (also known as syntactic unification), there exists always a unique unifier for solvable unification problems from which all other unifiers can be derived by instantiation. This unique (up to renaming) unifier is called the most general unifier, but for equational algebras the situation is completely different: the minimal complete set of unifiers is not always finite and it may not even exist, which was conjectured by Gordon Plotkin [63] in his seminal paper in 1972. This paper introduced the idea to take some troublesome axioms like associativity or commutativity out of the data base and to build them directly into the deduction machinery. Since then unification problems and equational theories have been classified with respect to the cardinality of their minimal complete set of unifiers. These results led to the development of general approaches and algorithms, which can be applied to a whole class of theories. This is the topic of universal unification, seee.g. [75, 80].


More specifically, a unification problem s =? t for two given terms s and t is the problem to find a unifier a such that s a = t a .A substitution a is more general than a substitution т if there is a substitution X such that т = a о X. We will also say a subsumes т. The unifier a is a most general unifier, if for any other unifier т of s and t we can find a substitution X such that т = a о X. We often have the need to limit the equality on substitutions to a set of variables and write a =V т if xa = x т for all variables x e V. Generalizing this notion to E -unification, where E is an equational theory, =E is equality under E and a is an E-unifier for s and t with sa =E ta, we may have more than one most general unifier. A minimal and complete set of E-unifiers, denoted xU ?E for s and t, is a set such that for every a e xU ?E we have sa =VE t a .Thesetis complete if for any E-unifier т there exists some a in xU ?E such that т =E a о X. The set xU ?E is minimal in the sense that for every two unifiers a, т in xU ?E there is no X with a =E т о X, that is all unifiers in x-U ?e are independent. We say that a unification problem is unitary if xU ?E is a singleton, it is finitary if xU ?E is finite for every s and t and it is infinitary if there are terms s and t such that xU ?E is infinite. Unfortunately there are theories such that two terms are unifiable, but the set xU ?E is not recursively enumerable. In this case we call the problem nullary or of type zero. This classification according to the type naturally leads to a hierarchy of equational theories called the unification hierarchy.

It turned out that this well established view of unification theory changes drastically, if we redefine the notion of a most general unifier. Recall that a unifier a subsumes another unifier т if:

Hence standard unification theory is based on the subsumption relation. We generalize this notion and define an encompassment relation on substitutions: a substitution a is encompassed by a substitution т, if there exist substitutions X1 and X2 such that

where X1 has to have certain properties to be defined in the next paragraph below. The idea is that X2 is used to establish the known subsumption relation between т and a as in standard unification theory and is composed as usual “from the right” in the tripartition X1 о a о X2. The substitution X1 allows us also to compose “from the left” and this can drastically reduce the cardinality of the set of minimal E-unifiers, which we now call essential E-unifiers: an E-unifier a is an essential E-unifier if for any other unifier т there exist substitutions X1 and X2 such that т =VE X1 о a о X2. We say т encompasses a and the set of essential E-unifiers, denoted as eU ?E, is the set of E-unifiers such that for any unifier т there is some a e eU ?E, such that т =E X1 о a о X2.

We say a unification problem is e-unitary (is e-finitary) if the set of essential unifiers is always a singleton (is always finite). A unification problem is e-infinitary (e-nullary) if there are two terms such that the set of essential unifiers is infinite (does not exist).

  • [1] First workshop in Val d’Ajol in 1987 and since then annually. Since 1997, there is a websiteUNIF1997, UNIF1998,UNIF1999upto UNIF2005 in Japan and UNIF2006 attheFLOC conferencein Seattle, UNIF2007 and UNIF2008 at the Schloss Hagenberg, Linz, Austria. The current UNIF’scan be found at UNIF2013, UNIF2014 and UNIF2015.
< Prev   CONTENTS   Source   Next >