Unification (logic)

Unification is a method of unifying predicate logic expressions. Two expressions are unified by replacing their variables with appropriate terms so that the resulting expressions are the same. Unification has gained greater importance, particularly in computer logic and computational linguistics. For example, uses the inference engine of the prologue - interpreter unification. In computational linguistics, there are so-called unification grammars that are based on this concept. Unification also plays a major role in theorem proving .

Unification is based on substitution as a basic operation . In the context of predicate logic, a substitution σ within a given expression means the replacement of a variable by a term in which this variable may not appear. The variable is to a certain extent "instantiated" by the term.

If a set of expressions is substituted by a substitution σ to an equivalent expression, i.e. H. , then σ is called the unifier of this set of expressions. The application of a unifier to this set is called unification. Not all expression sets can be unified. ${\displaystyle \{A_{1},A_{2},\ldots ,A_{n}\}}$ ${\displaystyle \sigma (A_{1})\equiv \sigma (A_{2})\equiv \cdots \equiv \sigma (A_{n})}$

example

Given are the expressions and . Uppercase letters stand for variables and lowercase letters for atomic expressions. ${\displaystyle A_{1}=\left(X,Y,f(b)\right)}$ ${\displaystyle A_{2}=\left(a,b,Z\right)}$

Substituting in now by , through and through , so they are the same or unified . You get ${\displaystyle A_{1}}$ ${\displaystyle X}$ ${\displaystyle a}$ ${\displaystyle Y}$ ${\displaystyle b}$ ${\displaystyle A_{2}}$ ${\displaystyle Z}$ ${\displaystyle f\left(b\right)}$

${\displaystyle \sigma (A_{1})=\left(a,b,f(b)\right)}$

${\displaystyle \sigma (A_{2})=\left(a,b,f(b)\right)}$

With

${\displaystyle \sigma =\{X\mapsto a,Y\mapsto b,Z\mapsto f(b)\}}$.

Smallest common unifier

There are usually several unifiers for a set of expressions. A unifier is called the smallest common unifier or the most general unifier if there is a substitution with for every other unifier . Of course, this is not necessarily unique. ${\displaystyle \mu }$ ${\displaystyle \sigma }$ ${\displaystyle \tau }$ ${\displaystyle \sigma =\tau \circ \mu }$

Using Robinson's algorithm after John Alan Robinson , one can find a smallest common unifier for unifiable expressions.

Unification algorithm

The following is a representation of the unification algorithm in pseudocode :

Eingabe: Menge von Ausdrücken A
Ausgabe: allgemeinster Unifikator sub

sub := ∅
while |sub(A)| > 1 do begin
  Durchsuche die Ausdrücke sub(A) von links nach rechts,
  bis die erste Position gefunden ist, wo sich zwei Ausdrücke
  in einem Zeichen unterscheiden.
  if keines der beiden Zeichen ist eine Variable then
    Gib "nicht unifizierbar" aus. STOP
  else begin
    Sei X die Variable und t der im anderen Ausdruck beginnende Term
    (kann auch Variable sein)
    if X kommt in t vor then
      Gib "nicht unifizierbar" aus. STOP
    else sub := sub[X/t] (sub und [X/t] werden hintereinander ausgeführt)
  end
end
Gib sub aus.

literature

• YES Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965 ACM Press
• Michael M. Richter. Artificial Intelligence Principles. Knowledge representation, inference and expert systems. Teubner Verlag, 1996. ISBN 3-519-12269-3 .
• Uwe Schöning : Logic for computer scientists . Spectrum Akademischer Verlag, Berlin 2005, ISBN 3-8274-1005-3 , pp. 90-93
• Baader, F. and W. Snyder, "Unification Theory" (PDF; 677 kB), chapter eight in Handbook of Automated Deduction , Springer Verlag, Berlin (2001).