Unification Algebras : an Axiomatic Approach to Unification, Equation Solving and Constraint Solving

Abstract

Abstract Traditionally unification is viewed as solving an equation in an algebra given an explicit construction method for terms and substitutions. We abstract from this explicit term construction methods and give a set of axioms describing unification algebras that consist of objects and mappings, where objects abstract terms and mappings abstract substitutions. A unification problem in a given unification algebra is the problem to find mappings for a system of equations 〈s_i= t_i | i ∈I〉, where si and ti are objects, such that si, and ti are mapped onto the same term. Typical instances of unification algebras and unification problems are: Term unification with respect to equational theories and sorts, standard equation solving in mathematics, unification in the λ-calculus, constraint solving, disunification, and unification of rational terms. Within this framework we give general purpose unification rules that can be used in every unification algorithm in unification algebras. Furthermore we demonstrate the use of this framework by investigating the analogue of syntactic unification and unification of rational terms.