Unification Theory

Franz BaaderFranz Baader, K.U. SchulzK.U. Schulz

Franz Baader, K.U. Schulz
Unification Theory
In W. Bibel and P.H. Schmidt, eds., Automated Deduction – A Basis for Applications, Vol. I: Foundations – Calculi and Methods, volume 8 of Applied Logic Series, 225-263. Kluwer Academic Publishers, 1998

Details
Bibtex

KurzfassungAbstract
In this chapter, we first motivate equational unification by its applications in theorem proving and term rewriting. In addition to applications that require the computation of unifiers, we will also mention constraint-based approaches, in which only solvability of unification problems (i.e., the existence of unifiers) must be tested. Then we extend the definitions known from syntactic unification (such as most general unifier) to the case of equational unification. It turns out that, for equational unification, one must be more careful when introducing these notions. In the third section, we will mention some unification results for specific equational theories. In the fourth, and central, section of this chapter, we treat the important problem of how to combine unification algorithms. This problem occurs, for example, if we have a unification algorithm that can treat the commutative symbol ``+ and another algorithm that can treat the associative symbol ``x, and we want to unify terms that contain both symbols. Finally, we conclude with a short section in which other interesting topics in the field of equational unification are mentioned, which could not be treated in more detail in this chapter.
Forschungsgruppe:Research Group: AutomatentheorieAutomata Theory

@incollection{ Baader-Schulz-ADHandbook98,
  address = {Dordrecht, NL},
  author = {F. {Baader} and K.U. {Schulz}},
  booktitle = {Automated Deduction -- A Basis for Applications, Vol.~I: Foundations -- Calculi and Methods},
  editor = {W. {Bibel} and P.H. {Schmidt}},
  pages = {225--263},
  publisher = {Kluwer Academic Publishers},
  series = {Applied Logic Series},
  title = {Unification Theory},
  volume = {8},
  year = {1998},
}