Unification in First-Order Logic (FOL)

Table of Content:

Content Highlight:

Unification in First-Order Logic (FOL) is a key process that makes two logical atomic expressions identical through substitution. The UNIFY algorithm matches two atomic sentences by finding a suitable substitution, or it fails if they don't match. Essential conditions for unification in First-Order Logic (FOL) include identical predicate symbols and the same number of arguments in both expressions. The Most General Unifier (MGU) is the simplest substitution that achieves this match. For example, UNIFY{King(x), King(John)} results in {x/John}, successfully unifying the expressions. Understanding unification in First-Order Logic (FOL) and mastering the UNIFY algorithm are crucial for effective logical inference in FOL.

What is Unification in FOL?

Unification in First-Order Logic (FOL) is a crucial process that makes two different logical atomic expressions identical by finding a suitable substitution. This process relies on substitution, where variables in the expressions are replaced to achieve uniformity.

Unification takes two literals as input and attempts to make them identical through substitution. Formally, let Ψ1 and Ψ2 be two atomic sentences and 𝜎 be a unifier such that Ψ1𝜎 = Ψ2𝜎. This can be expressed as UNIFY(Ψ1, Ψ2).

Example:

Let's find the Most General Unifier (MGU) for the following expressions:

UNIFY{King(x), King(John)}

Given:

  • Ψ1 = King(x)
  • Ψ2 = King(John)

The goal is to find a substitution 𝜎 that makes Ψ1 and Ψ2 identical.

Solution:

To unify Ψ1 and Ψ2, we can substitute the variable x with the constant John. Therefore, the substitution 𝜎 is {x/John}.

Applying this substitution:

Ψ1𝜎 = King(x){x/John} = King(John)
Ψ2𝜎 = King(John){x/John} = King(John)

Since Ψ1𝜎 = Ψ2𝜎, the unification is successful, and {x/John} is the Most General Unifier (MGU).

Let Ψ1 = King(x), Ψ2 = King(John),

Substitution θ = {John/x} is a unifier for these atoms, and applying this substitution, both expressions will be identical.

The UNIFY Algorithm:

The UNIFY algorithm is used for unification. It takes two atomic sentences and returns a unifier for those sentences (if any exist). Unification is a key component of all first-order inference algorithms. It returns fail if the expressions do not match. The substitution variables are called the Most General Unifier or MGU.

Additional Example:

Consider two different expressions, P(x, y) and P(a, f(z)).

To make both statements identical, we will perform the necessary substitution.

In summary, unification in FOL is the process of making two atomic expressions identical by finding appropriate substitutions, ensuring that the expressions can be matched or unified.

Conditions for Unification:

Here are some basic conditions that must be met for unification:

  • The predicate symbol must be the same in both expressions. Atoms or expressions with different predicate symbols cannot be unified.
  • The number of arguments in both expressions must be identical.
  • Unification will fail if there are two identical variables present in the same expression.

Unification Algorithm

Algorithm: Unify(Ψ1, Ψ2)

  1. If Ψ1 or Ψ2 is a variable or constant, then:
    • a) If Ψ1 and Ψ2 are identical, return NIL.
    • b) If Ψ1 is a variable:
      • i. If Ψ1 occurs in Ψ2, return FAILURE.
      • ii. Otherwise, return {Ψ2 / Ψ1}.
    • c) If Ψ2 is a variable:
      • i. If Ψ2 occurs in Ψ1, return FAILURE.
      • ii. Otherwise, return {Ψ1 / Ψ2}.
    • d) Otherwise, return FAILURE.
  2. If the initial predicate symbol in Ψ1 and Ψ2 are not the same, return FAILURE.
  3. If Ψ1 and Ψ2 have a different number of arguments, return FAILURE.
  4. Set the substitution set (SUBST) to NIL.
  5. For i = 1 to the number of elements in Ψ1:
    • a) Call the Unify function with the ith element of Ψ1 and the ith element of Ψ2, and put the result into S.
    • b) If S equals FAILURE, return FAILURE.
    • c) If S is not NIL, then:
      • i. Apply S to the remainder of both Ψ1 and Ψ2.
      • ii. Append S to SUBST.
  6. Return SUBST.

Implementation of the Unification Algorithm

  1. Initialize the substitution set to be empty.
  2. Recursively unify atomic sentences by following these steps:
    1. Check for identical expressions:
      • If the expressions are identical, no substitution is needed.
    2. Handle variables:
      • If one expression is a variable vi and the other is a term ti that does not contain the variable vi, then:
        • Substitute ti / vi in the existing substitutions.
        • class="mt-3"Add ti / vi to the substitution set.
    3. Handle functions:
      • If both expressions are functions, then:
        • The function names must be identical.
        • The number of arguments must be the same in both expressions.
  3. For each pair of atomic sentences, find the most general unifier (if one exists).

Examples of Finding the Most General Unifier (MGU)

  1. Find the MGU of {p(f(a), g(Y)) and p(X, X)}:

    Here, Ψ1 = p(f(a), g(Y)) and Ψ2 = p(X, X)

    Step 1: Substitute X with f(a)

    SUBST θ = {f(a) / X}

    Step 2: Now Ψ1 = p(f(a), g(Y)) and Ψ2 = p(f(a), f(a))

    Unification fails because g(Y) cannot be unified with f(a).

    Result: Unification is not possible for these expressions.

  2. Find the MGU of {p(b, X, f(g(Z))) and p(Z, f(Y), f(Y))}:

    Here, Ψ1 = p(b, X, f(g(Z))) and Ψ2 = p(Z, f(Y), f(Y))

    Step 1: Substitute Z with b

    SUBST θ = {b / Z}

    Step 2: Now Ψ1 = p(b, X, f(g(b))) and Ψ2 = p(b, f(Y), f(Y))

    Substitute X with f(Y)

    SUBST θ = {f(Y) / X}

    Step 3: Now Ψ1 = p(b, f(Y), f(g(b))) and Ψ2 = p(b, f(Y), f(Y))

    Substitute Y with g(b)

    SUBST θ = {g(b) / Y}

    Result: Successfully unified. Unifier = {b / Z, f(Y) / X, g(b) / Y}.

  3. Find the MGU of {p(X, X) and p(Z, f(Z))}:

    Here, Ψ1 = p(X, X) and Ψ2 = p(Z, f(Z))

    Step 1: Substitute X with Z

    SUBST θ = {X / Z}

    Step 2: Now Ψ1 = p(Z, Z) and Ψ2 = p(Z, f(Z))

    Unification fails because Z cannot be unified with f(Z).

    Result: Unification is not possible for these expressions.

  4. Find the MGU of UNIFY(prime(11), prime(y)):

    Here, Ψ1 = prime(11) and Ψ2 = prime(y)

    Step 1: Substitute y with 11

    SUBST θ = {11 / y}

    Result: Successfully unified. Unifier = {11 / y}.

  5. Find the MGU of Q(a, g(x, a), f(y)) and Q(a, g(f(b), a), x):

    Here, Ψ1 = Q(a, g(x, a), f(y)) and Ψ2 = Q(a, g(f(b), a), x)

    Step 1: Substitute x with f(b)

    SUBST θ = {f(b) / x}

    Step 2: Now Ψ1 = Q(a, g(f(b), a), f(y)) and Ψ2 = Q(a, g(f(b), a), f(b))

    Substitute y with b

    SUBST θ = {b / y}

    Result: Successfully unified. Unifier = {f(b) / x, b / y}.

  6. Find the MGU of UNIFY(knows(Richard, x), knows(Richard, John)):

    Here, Ψ1 = knows(Richard, x) and Ψ2 = knows(Richard, John)

    Step 1: Substitute x with John

    SUBST θ = {John / x}

    Result: Successfully unified. Unifier = {John / x}.