Skip to main content

Well Form Formula

 Well Form Formula (WFF):


WFF are defined recursively as follows:
  • an atomic formula is WFF
  • if P and Q are WFF, ∽P, P & Q,  P V Q, P⇾Q, P↔Q, ∀x P(x), ∃x P(x) are WFF`s.
  • WFF are formed only by applying the above rules a finite of times.

Properties of WFF:
  1.  P & ∽P are inconsistent and P V∽P valid, Since the first one is false under every interpretation and the second one is true under every interpretation.
  2. From 2 WFF:       
                                    CLEAVER (Bill) 
                         ∀x  CLEAVER(x)    → SUCCESS(x)
                                   SUCCESS(Bill)
    Which is a logical consiquence.
  3.  Inference Rule: Assertion : LION (leo)
                               Implecation: ∀x LION(x) ⇾PHEROSUS(x)
                               Conclusion: PHEROSUS(Leo)
    in general:
                       P(a)
           ∀x  P(a)  ⇾ Q(x)
           ----------------------
                     Q(a)
  4. Unification Rule: Any Substitution that makes two or more equations equal is called  'Unifier' for that equation. Applying a substitution to an expression E, Produces an instance E`(E) where           E` = E.β. Given two expressions that are unifiable such as C1 and C2 with the unifier β with C1.β = C2 where β is the most general unifier if any other unifier α is an instance of β.

    Example: 
       P(u, b , v ) and 
       P(a, x, y)
       α { a/u , b/x, v/y}
       β {a/u, b/x, c/v, c/y}
     α is most general unifier (MGU) 
  5. Resolution Principle: Given clauses C1 and C2 with no variable in common if there is a literal L1 in C1 which is a complement of literal L2 in C2 both L1 and L2 are deleted and C is formed for the remaining reduced clauses. Now is called resolvent of C1 and C2.
           ∽P V Q  and  ∽Q V R
                     ∽PVR       


  6.  Binary Resolution: Two clauses having complementary literals are combined to produce a single clause after deleting the complementary literals. 

     ∽P (x,a) V Q(x) and  ∽Q(b) V R(x)
    -------------------------------------------
                     ∽P(b,a) V R(b)            

    with substitution {b/x}
Problem: Find Unifier:
       
{∽MARRIED (x,y) V ∽ MOTHER (x,y) V Father(y,z),
     MARRIED (Sue, Joe)∽FATHER (Joe, Bill)}

Unifer β = {x/Sue, y/Bill, z/Joe}





All Topics:

Comments

Post a Comment