Unification . Unification is a process that allows, by substituting variables for terms, to obtain, from a pair of formulas , a third one that will be true whenever any of the first ones is. This feature makes unification a very useful tool in the formal proof of theorems. Let’s see the necessary foundations to carry out this process.
Summary
[ hide ]
- 1 Substitution
- 2 Composition of substitutions
- 3 Unifier and more general unifier
- 4 Robinson’s Unification Algorithm
- 5 Bibliography
- 6 Sources
Substitution
The first concept related to unification is that of substitution.
A finite set of the form {t1 / v1, …, tn / vn} is called a substitution, where each vi is a variable, each ti is a different term from vi and for 1 <i, j <n, i ǂ j , I saw ǂ vj.
Examples of substitutions are:
- {a / x, f (b) / y}
- {y / x, b / z}
- {b / x, b / y, f (a) / z}
They are not substitutions:
- {a / x, b / x}; the variable x appears replaced by two different terms
- {a / x, y / y, f (a) / z}; the variable y appears replaced by itself.
- {a / b, y / y, f (a) / z}; b cannot be substituted since it is not a variable.
The utility of substitutions is that you can obtain, from a substitution and a formula , a new formula that will be true as long as the first one is true, this is called applying the substitution to the formula and denotes Fσ, where F is the formula and σ is the substitution.
The procedure to obtain Fσ is very simple and consists of substituting in F, all the occurrences of variables that appear in σ, by the corresponding term in σ itself.
The following example illustrates how to apply a substitution to a formula:
Let F = A (x, f (y), g (z)) and σ = {a / z, f (b) / x}. To obtain Fσ the variables of F are analyzed, firstly x appears, as x is substituted in σ by f (b), we proceed to substitute it in F, obtaining:
A (f (b), f (y), g (z))
If x had other occurrences in F, it should be replaced in all of them by f (b), but since this is not the case, we proceed directly to analyze the next variable of F. The variable y is not substituted in σ by what is left intact in F, passing to the analysis of the last variable, z, the one that appears in σ replaced by a, which finally makes it: Fσ = A (f (b), f (y), g ( to))
Composition of substitutions
Two substitutions can be made up to obtain a new one. If σ and σ ‘are substitutions, the composition of σ and σ’ is denoted as σσ ‘and is the result of applying σ’ to all the terms of σ, adding to the resulting set all the elements of σ ‘whose variables are not found between the variables of σ and finally eliminate all the elements ti / vi that satisfy that ti = vi.
The following example illustrates how to compose substitutions:
Let σ = {v / x, w / y, f (a) / z} and σ ‘= {y / w, a / v, b / z, f (b) / u}
To obtain σσ’ the first step is to apply σ ‘to all terms of σ, which in this case are v, w and f (a). The result is {a / x, y / y, f (a) / z}.
The second step is to add y / w, a / v and f (b) / u to the set since w, v and u do not appear among the variables of σ, resulting in {a / x, y / y, f (a) / z, y / w, a / v, f (b) / u}
Finally, y / y is eliminated so we obtain: σσ ‘= {a / x, f (a) / z, y / w, a / v, f (b) / u}
Unifier and more general unifier
There are pairs of formulas from which the same result can be obtained, applying a certain substitution to both. In such cases the formulas are said to be unifiable and the substitution is called unifying.
Below are two pairs of unifiable formulas and their respective unifiers:
- F1a = Q (x, b) F1b = Q (a, y) σ = {a / x, b / y}
F1aσ = F1bσ = Q (a, b) - F2a = R (f (y), x) F2b = R (z, f (a)) σ = {f (y) / z, f (a) / x}
F2aσ = F2bσ = R (f (y), fa))
The usefulness of unifiers in proving theorems is that the formula obtained by applying the unifier to a unifiable pair is a logical consequence of both pair formulas. In other words, it is true whenever any of these is true, or even more useful, if it is false, it can be said that the original ones are also true, which is used in the proof by refutation, which will be studied later.
When a pair of formulas is unifiable, it is possible to find an infinite set of unifiers, some much simpler than others. Of course, when using a unifier, it is highly desirable that it be as simple as possible, this is called a more general unifier (UMG) and is defined as:
If A and B are formulas, γ is said to be the UMG of A and B if for all σ, unifier of A and B, there exists a substitution σ ‘such that Aσ = Aγσ’
Robinson’s Unification Algorithm
The UMG definition does not directly state how to find it, which is what is really needed.
Following is a method, known as Robinson’s unification algorithm, which, given two formulas A and B, allows us to determine if they are unifiable and in such a case find their UMG. Before describing the algorithm , a definition must be introduced:
Let A and B be formulas, the set consisting of the first two terms in which A and B differ is called the disagreement set (D).
Examples:
- A = P (x, f (y)) B = P (x, f (y)) D = {}
- A = P (x, f (y)) B = P (z, f (a)) D = {x, z}
- A = R (x, f (a)) B = R (g (a), g (y)) D = {x, g (a)}
- A = P (a, g (y)) B = P (a, f (a)) D = {g (y), f (a)}
- A = P (f (a), g (y)) B = P (f (x), f (a)) D = {a, x}
It is important to note the difference between situations of the type present in Example 4, and of the type present in Example 5.
In the first case, the difference is in the function symbols (f and g), so in D there are both symbols with their respective arguments, however, in the second case, the function symbols are identical, the difference being in the arguments (ayx).
Robinson’s Unification Algorithm:
- Input: A and B formulas.
- – k = 0, σ0 = {}
- – If Aσk = Bσ’k, then end: UMG = σk.
otherwise Find Dk, set disagreement of Aσk and Bσk. - -If there is in Dk a variable (v) and a term (t) such that v does not occur in t,
then:
- σk + 1 = σk {t / v},
k = k + 1, go to step 2. Otherwise end: A and B are not unifiable. It can be said that the algorithm consists of constructing the UMG iteratively, from the disagreement set.
In each iteration, the substitution built up to that moment is applied to both formulas, if the same result is obtained, the UMG has already been found. Otherwise, the disagreement set is sought, not from A and B, but from the result of applying the substitution to each one. This last detail is very important, because if it is not taken into account, the same set of disagreements would always be obtained and the algorithm would not end.
Once the disagreement set (D) has been calculated, it is examined for a variable (v) and a term (t) where v does not occur, where the following situations can occur:
- D = {v1, v2}, where v1 ǂ v2 and both are variables. One can be taken as v and the other as t (of course, variables are also terms).
- D = {v ‘, t’}, where v ‘is a variable and t’ a constant or function that does not have v ‘as its argument. You take av ‘as vyt’ as t.
- D = {v ‘, t’ (v ‘)}, where v’ is a variable and t ‘a function whose argument is v’. A and B are not unifiable.
- D = {t₁, t₂}, where neither t₁ nor t₂ are variables. A and B
are not unifiable . If v and t were found, then the new substitution is constructed as the composition of the previous one with {t / v} and a new iteration is left.
Below are two examples where the algorithm is applied to a pair of formulas, in the first case unifiable and the second not:
First case .
A = R (x, f (a)) B = R (b, z)
First iteration .
k = 0 σ0 = {}
Aσ0 = A Bσ0 = B Aσ0 ǂ Bσ0
D0 = {x, b} v = xt = b
Second iteration .
k = 1 σ1 = {} {b / x} = {b / x}
Aσ1 = R (b, f (a)) Bσ1 = R (b, z) Aσ1 ǂ Bσ1
D0 = {f (a), z} v = zt = f (a)
Third iteration.
k = 2 σ2 = {b / x} {f (a) / z} = {b / x, f (a) / z}
Aσ2 = R (b, f (a)) Bσ2 = R (b, f ( a)) Aσ2 = Bσ2
The UMG is {b / x, f (a) / z}
Second case.
A = R (x, f (x)) B = R (z, z)
First iteration .
k = 0 σ0 = {}
Aσ0 = A Bσ0 = B Aσ0 ǂ Bσ0
D0 = {x, z} v = xt = z
Second iteration.
k = 1 σ1 = {} {z / x} = {z / x}
Aσ1 = R (z, f (z)) Bσ1 = R (z, z) Aσ1 ǂ Bσ1
D0 = {f (z), z} the variable occurs in the term, A and B are not unifiable.
