Resolution in the Predicate Calculus

RESOLUTION IN THE PREDICATE CALCULUS 

Unification

• Wffs can be abbreviated from ( ∀r₁, r₂,..... r_n) (λ₁v λ₂ v...... v λ_k) to λ₁v λ₂ v...... v λ_kthe variables r₁, r₂,..... r_n may occur in the literals λ₁v λ₂ v...... v λ_k. These abbreviated wffs are called clauses. 
• We can resolve two clauses containing matching but complementary literals. 
• That is if we have one literal as λ(r) and other as ᆨλ(τ) where τ is a term which does not contain r, then τ is substituted in place of r at the place it occurred, after this proposition resolution is performed on complementary literals so that a resolvent of two clauses is obtained. 
• Example: If P(f(x), A) v Q(B, C) and ᆨP(y, A) v R(y, C) v S(A, B) are two clauses. 
• We substitute f(x) in place of x in the second clause we have,
• ᆨP(f(x), A) v R(f(x), C) v S(A, B) 
• Now these two clauses can be resolved to get,
• ᆨR(f(x), C) v S(A, B) v Q(B, C) 
• The process of computing appropriate substitution is done by unification. 
• In AI unification is a very important process. . 
• Substitution Instance: It is the expression obtained by substituting terms in place of variables in an expression. 

                Example: Given expression Q[x, f(y), B] 

                we have, 

                Q[z, f(w), B] 

                Q[z, f(A), B] 

                Q[g(z), f(A), B] 

                Q[C, f(A), B] 

    The first three are alphabetic variants of the given expression as variables are substituted in the original expression. 

• Ground Instance: The expression Q[C, f(A), B] is a ground instance of Q[x, f(y), B] since it does not contain any variables. 
• The substitution can be shown by using a set of ordered pairs, 

                S = {τ₁/r₁, τ₂/r₂, ....... τ_n/r_n} 

• The substitutions made in the above example of Q[x, f(y), B] are, 

                S₁ = {z/x, w/y}, S₂ = {A/y}, S₃ = {g(z)/x, A/y}, and. S₄ = {C/x, A/y}. 

• If we want to do a substitution S is a wff w then it can be represented as ωs, 

                Q[g(z), f(A), B] = Q[x, f(y), B] S₃ 

• A substitution S₁, S₂ that is combination of S₁ and S₂ is done by first substituting S₂ in S₁. 
• Now S₂ may have substitution for other variables which may not present in S₁ so they are added to the obtained substitution. 

                Example: If S₁ is {f(y, z)/x} and S₂ is {A/x, B/y, C/w, D/z} first of all, S₂ is applied to S, so we have, {f(y, z)/x} = {f(A, B)/x} 

                Now, the substitution of variables not occurred in S₂ and present in S₂ are add to above result. 

                        ∴ {f(y, z)/x} {A/x, B/y, C/w, D/z} = {f(A, B)/x, B/y, C/w, D/z}

• Composition of substitutions are associative i.e. (S₁ S₂) S₃ = S₁(S₂ S₃) 

                Proof: Let w be Q(y, z), S₁ be {f(z)/y} and S₂ be {A/z} 

                Then,

                (w S₁) S₂ = [Q(f(z), z] 

                                = Q(f(a), A) 

                w(S₁ S₂)  = [Q(y, z)] [f(A).y, A/z] 

                                = Q[f(A), A) 

                Hence proved.

• Composition of substitution are not commutative i.e., S₁S₂ ≠ S₂S₁  

                Proof: By taking an example we will prove this, where w be Q(y, z), S₁ be {f(z)/ y} and S₂ be {A/z}

                w(S₁S₂) = Q(f(A), A) 

                w(S₂S₁) = [Q(y, z)] [A/z, f(z)/y] 

                              = Q(f(z), A) 

                As Q(f(A), A) Q(f(z), A) 

                Substitutions are not commutative. 

                Therefore, order of application of substitutions is important to be considered. 

• Now, the substitution be applied to a set w₁ which consists of a set of expressions and denoted by {w_i}S where S is the substitution made. 
• If a substitution S exists such that w₁S = w₂S = .... Then {w_i is called unifiable set and S is called unifier of {w₁} 

                Example: S = {C/z, D/y} unifies {Q[y, f(z), D], Q[Y, f(C), D]} to give {Q[D, f(C), D]}. 

• From the example, we observe that there is no need to substitute D/y for unifying the sets given. So S = {C/z, D/y} is not a simplest unifier. 
• mgu: It is the most general or simpler unifier. 
• Property of g of {w₁}: if {w₁} has a unifier named S which gives {w₁}S on substitution, then there will be a substitution S¹ such that {w₁}S = {w₁} gS¹. 
• The most general unifier produces a common instance is unique except the alphabets may change. 

UNIFY Algorithm 

• Several algorithms are used to find the most general unifier and it unifying is not possible it returns failure UNIFY is are amount them. 
• UNIFY algorithm every literal and every term is represented as a list and it works on these list structure expressions. 
• Example: ᆨQ(z, g(A, y)) is written as (ᆨQ z (g A y) where ᆨQ is the third top-label expression 

Disagreement Set 

• It is the basic idea used in UNIFY Algorithm. 
• It is obtained from a non-empty set W of expressions, by finding the first symbol in where that is not Same in all expressions and then the symbol at that position from all the expressions forms a sub expression, this expression is called the disagreement set. 
• Example: In lists [(ᆨQ z (g A y), (ᆨQ z (g x B)] 
• The disagreement set is {A, .x} 
• By substituting A for x this can be brought to an agreement. 
• The algorithm for where Γ is a set of list-structured expressions is as follows, 

UNIFY(Γ) 

1. i ←0, Γ_i < Γ, σ ← ∈ (here i is initialized to 0, Γ_i to Γ and an empty substitution is made for σ_i) 
2. ^Tf Γ_iis a singleton, exit withσ_i the mgu of Γ. Otherwise, continue. 
3. D_i  ← the disagreement set of Γ_i
4. If these exists elements u_i and p_i, in D₁ such that u₁, is a variable that does not occur in p₁, continue. Else, exist with failure that Γ is not unifiable.
5. {σ_i+1 ←  σ_i p_k/u_k}, Γ_i+1  ← Γ_i{p_k/u_k} (here it has to be noted that Γ_i+1 = Γ_i = σ_i+1)
6. i ← i + 1 
7. Go to step 2. 

• The algorithm finds a mgu of a set or else returns i saying the set is not unifiable. 
• The mgu produced can easily be converted into first-order logic form.