• Unification is the process of finding legal substitutions that make different logical expressions look identical.
• It is a recursive algorithm.
• The algorithm statement is as follows –
Unify (L1, L2) = θ where
SUBST (θ, L1) = SUBST (θ, L2)
Algorithm/Steps:
1. If L1 and L2 are both variables or constants, then:
a. If L1 and L2 are identical, return NIL
b. Else if L1 is a variable, then if L1 occurs in L2, return {FAIL}. Else return (L2/L1).
c. Else if L2 is a variable, then if L2 occurs in L1, return {FAIL}. Else return (L1/L2).
d. Else return {FAIL}.
2. If initial predicate symbols in L1 and L2 are not identical, then return {FAIL}.
3. If L1 and L2 have different no. of arguments, return {FAIL}.
4. Set SUBST to NIL.
5. For i 1 to no. of arguments in L1:
a. Call Unify with the ith argument of L1 and L2, putting result in S.
b. If S contains FAIL, return {FAIL}.
c. If S is not equal to NIL, then:
i. Apply S to the remainder of both L1 and L2.
ii. SUBST:=APPEND (S, SUBST)
6. Return SUBST.
Steps to convert predicate logic to clause form:
1. Elimination of implication, i.e. Eliminate all ‘à’: Replace PàQ with ¬P˅Q.
2. Distribute negations: Replace ¬¬P with P, ¬(P˅Q) with ¬P˄¬Q and so on.
3. Eliminate existential quantifiers by replacing them with Skolem constants or Skolem functions:
Ex.: ∀X∃Y(P1(X, Y)⋁(P2(X, Y)) ≡ ∀X(P1(X, f(X))⋁(P2(X, f(X)))
4. Rename variables to avoid duplicate quantifiers.
5. Drop all universal quantifiers.
6. Place expression into C conjunctive Normal Form.
7. Convert to clauses.
8. Rename variables to avoid duplicate clauses.
No comments:
Post a Comment