Unification (computer science)

Unification is a method of unification predicate logic expressions. Two expressions are unified by their variables are replaced by appropriate terms, that the resulting expressions are equal. The unification in particular has become more important in the computer logic and computational linguistics. So for example uses the inference engine of Prolog interpreter unification. In computational linguistics, there are so-called Unifikationsgrammatiken, based on this concept. Even when unification theorem plays an important role.

As a basic operation of unification is the substitution basis. In the context of predicate logic, a substitution σ is the substitution of a variable by a term in which this variable must not occur within a given expression. The variable is somehow " instantiated " by the term.

Is a set of expressions substituted by a substitution σ to an equivalent expression, i.e., it is referred as a unifier σ, this expression amount. The application of a unifier on this quantity is called unification. Not all expression levels can be unified.

Example

Given the expressions and. Uppercase letters stand for variables and lowercase letters for atomic expressions.

If we replace by in now, by and by, so they are the same or unified. obtained

With

The lowest common unifier

To a set of expressions usually are several unifiers. This is called a unifier unifier lowest common or general unifier, if it is for every other unifier is a substitution with. This of course is not necessarily unique.

Using the algorithm of Robinson by John Alan Robinson can be found to unifizierbaren expressions a lowest common unifier.

Unification algorithm

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

Input: A set of expressions Edition: general unifier sub sub: = ∅ while | sub ( A) |> 1 do begin    Search the expressions sub ( A) from left to right,    to the first position is found where two expressions    differ in one character.    if neither of the two characters is a variable then      Give " not unifiable " from. STOP    else begin      Let X be the variable t and the beginning in the other expression Term      ( may be variable)      if X occurs in t before then        Give " not unifiable " from. STOP      else sub: = sub [ X / t] ( sub and [X / t] to execute the same )    end end Give from sub. literature

  • J. A. Robinson. A Machine - Oriented Logic Based on the Resolution Principle. Journal of the ACM. 1965 ACM Press
  • Michael M. Richter. Principles of Artificial Intelligence. Knowledge representation, inference and expert systems. Teubner Verlag, 1996. ISBN 3-519-12269-3.
  • Uwe Schöning: Logic for Computer. Spektrum Akademischer Verlag, Berlin 2005, ISBN 3-8274-1005-3, p.90 -93
  • Logic
Interpreter (computing) Substitution (logic)
48619
de