Scribd Logo
Upload

Welcome to Scribd!

  • 46 views

    Predicate Calculus: Conversion To Normal Form

    Uploaded by

    Archana Panwar
    The document describes the steps to convert a first-order logic formula to clause normal form: 1) Eliminate redundant quantifiers and introduce existential quantifiers for unhandled variables 2) Rename variables quantified more than once 3) Eliminate implications 4) Move negations inward 5) Push quantifiers to the right 6) Eliminate existential quantifiers through Skolemization 7) Move universal quantifiers left 8) Distribute conjunction over disjunction 9) Optionally simplify

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd

    Predicate Calculus: Conversion To Normal Form

    Uploaded by

    Archana Panwar
    46 views25 pages
    The document describes the steps to convert a first-order logic formula to clause normal form: 1) Eliminate redundant quantifiers and introduce existential quantifiers for unhandled variables 2) Rename variables quantified more than once 3) Eliminate implications 4) Move negations inward 5) Push quantifiers to the right 6) Eliminate existential quantifiers through Skolemization 7) Move universal quantifiers left 8) Distribute conjunction over disjunction 9) Optionally simplify

    Original Title

    16 - Clausal Form

    Copyright

    © © All Rights Reserved

    Available Formats

    PPTX, PDF, TXT or read online from Scribd

    Did you find this document useful?

    Is this content inappropriate?

    The document describes the steps to convert a first-order logic formula to clause normal form: 1) Eliminate redundant quantifiers and introduce existential quantifiers for unhandled variables 2) Rename variables quantified more than once 3) Eliminate implications 4) Move negations inward 5) Push quantifiers to the right 6) Eliminate existential quantifiers through Skolemization 7) Move universal quantifiers left 8) Distribute conjunction over disjunction 9) Optionally simplify

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd
    Download as pptx, pdf, or txt
    46 views25 pages

    Predicate Calculus: Conversion To Normal Form

    Uploaded by

    Archana Panwar
    The document describes the steps to convert a first-order logic formula to clause normal form: 1) Eliminate redundant quantifiers and introduce existential quantifiers for unhandled variables 2) Rename variables quantified more than once 3) Eliminate implications 4) Move negations inward 5) Push quantifiers to the right 6) Eliminate existential quantifiers through Skolemization 7) Move universal quantifiers left 8) Distribute conjunction over disjunction 9) Optionally simplify

    Copyright:

    © All Rights Reserved
    Download as PPTX, PDF, TXT or read online from Scribd
    Download as pptx, pdf, or txt
    of 25

    Predicate Calculus

    Conversion to Normal Form


    Inference Rules
     Universal elimination:
    x Likes( x, IceCream) with the substitution {x / Einstein} gives us
    Likes(Einstein, IceCream)
    The substitution has to be done by a ground term
     Existential elimination: (Skolemization)
    From x Likes( x, IceCream) we may infer Likes(Man, IceCrea) as
    long as Man does not appear elsewhere in the Knowledge base
     Existential introduction:
    From Likes( Monalisa , IceCream) we can infer
    x Likes( x, IceCream )
    Basic Steps
     Convert the set of rules and facts into clause form
    (conjunction of clauses/disjunction of clauses)
     Insert the negation of the goal as another clause

     Use resolution to deduce a refutation

    If a refutation is obtained, then the goal can be


    deduced from the set of facts and rules.
    Conversion to Normal Form
     A formula is said to be in clause form if it is of the form:
    x1 x2…… xn[C1C2  …… Ck]
     All first order logic formulas can be converted to clause
    form
     We shall demonstrate the conversion on the formula:
    x {p(x) z { ¬y [q(x,y) p(f(x1)] y
    [q(x,y)p(x)] }}
    Conversion to Normal Form
     Step1:Take the existential closure and eliminate redundant
    quantifiers. This introduces x1 and eliminates and z, so:
    x {p(x) z { ¬y [q(x,y) p(f(x1)] y
    [q(x,y)p(x)] }}

    x1 x {p(x)  { ¬y [q(x,y)  p(f(x1)] y [q(x,y)


     p(x)] }}
    Conversion to Normal Form
     Step2 : Rename any variable that is quantified more than
    once. y has been quantified twice, so:
    x1 x {p(x)  { ¬y [q(x,y)  p(f(x1)] y [q(x,y) 
    p(x)] }}

    x1 x {p(x)  { ¬y [q(x,y)  p(f(x1)] z [q(x,z)


    p(x)] }}
    Conversion to Normal Form
     Step3 : Eliminate Implication.
    x1 x {p(x)  { ¬y [q(x,y)  p(f(x1))] z
    [q(x,z) p(x)] }}

    x1 x {¬p(x)  {¬y [¬q(x,y)  p(f(x1))] z


    [¬ q(x,z)  p(x)] }}
    Conversion to Clausal Form
     Step4 : Move the negation all the way inwards
    x1 x {¬p(x)  {¬y [¬q(x,y)  p(f(x1))] z
    [¬ q(x,z)  p(x)] }}

    x1 x {¬p(x)  { y [q(x,y)  ¬p(f(x1))]  z


    [¬q(x,z)  p(x)] }}
    Conversion to Clausal Form
     Step5 : Push the quantifiers to the right
    x1 x {¬p(x)  { y [q(x,y)  ¬p(f(x1))] z [¬q(x,z)
     p(x)] }}

    x1 x{¬p(x)  {[y q(x,y)  ¬p(f(x1))]  [z¬q(x,z)


     p(x)] }}
    Conversion to Normal Form
     Step6 : Eliminate Existential Quantifiers
    (Solemnization)
     Pick out the left most yB(y) and replace it with
    B(f(xi1,xi2,xi3….. xin)) where:
    1. xi1,xi2,xi3….. xin are all the free variables of yB(y) that are
    universally quantified to the left of yB(y) and,
     f is any n-ary function constant which does not occur
    already
    Conversion to Normal Form
     Skolemization
    x1 x{¬p(x)  {[y q(x,y)  ¬p(f(x1))] 
    [z¬q(x,z)  p(x)] }}

    x {¬p(x)  {[q(x,g(x))  ¬p((f(a))]  [z¬q(x,z)


     p(x)] }}
    Conversion to Normal Form
     Step7 : Move all universal quantifiers to the left
    x {¬p(x)  {[q(x,g(x))  ¬p((f(a))]  [z¬q(x,z)
     p(x)] }}

    x z {¬p(x)  {[q(x,g(x))  ¬p((f(a))] 


    [¬q(x,z)  p(x)] }}
    Conversion to Normal Form
     Step8 : Distribute  over 
    x z {¬p(x)  {[q(x,g(x))  ¬p((f(a))]  [¬q(x,z) 
    p(x)] }}

    x z {[¬p(x)  q(x,g(x))] 
    [¬p(x)  ¬p((f(a))] 
    [¬p(x)  ¬q(x,z)  p(x)] }
    Conversion to Normal Form
     Step9 : Simplify (Optional)
    x z {[¬p(x)  q(x,g(x))] 
    [¬p(x)  ¬p((f(a))] 
    [¬p(x)  ¬q(x,z)  p(x)] }

    x z {[¬p(x)  q(x,g(x))] 
    [¬p(x)  ¬p((f(a))] 
    [¬q(x,z)] }
    Summarize
     Step1:Take the existential closure and eliminate redundant quantifiers and
    introduce existential closure to unhandled variables.
     Step2: Rename any variable that is quantified more than once.
     Step3: Eliminate Implication.
     Step4: Move the negation all the way inwards.
     Step5: Push the quantifiers to the right.
     Step6: Eliminate Existential Quantifiers (Solemnization)
     Step7: Move all universal quantifiers to the left.
     Step8: Distribute  over 
     Step9: Simplify (Optional)
    Exercise
     x y z Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)
     x y married(x,y)  member(x)  member(y)
     x y z y a father(x,z)  father(z,y) 
    grandfather(x,y)
     x z bird(x)  fly(x)
    Step1:eliminate redundant introduce existential to
    unhandled variables

     xyz Gaul(x)  Potion(y) 


    Hostile(z)  Sells(x,y,z)  Criminal(x)
     x y married(x,y)  member(x)  member(y)
     x z father(x,z)  yfather(z,y) 
    grandfather(x,y)
     x bird(x)  fly(x)
    Step2: Rename any variable that is quantified more
    than once

     x y z Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)
     x y married(x,y)  member(x)  member(y)
     x y z father(x,z)  father(z,y) 
    grandfather(x,y)
     x bird(x)  fly(x)
    Step3: Eliminate Implication
     x y z {{Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)}  Criminal(x)}
     x y { {married(x,y)  member(x)}  member(y)}

     x y z { {father(x,z)  father(z,y)} 

    grandfather(x,y)}
     x { bird(x)  fly(x)}
    Step4: Move the negation all the way inwards
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x y {married(x,y)  member(x)  member(y)}

     x y z {father(x,z)  father(z,y) 

    grandfather(x,y)}
     x {bird(x)  fly(x)}
    Step5: Push the quantifiers to the right
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x y {married(x,y)  member(x)  member(y)}

     x y z {father(x,z)  father(z,y) 

    grandfather(x,y)}
     x {bird(x)  fly(x)}
    Step6: Eliminate Existential
    Quantifiers
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x {married(x,f(x))  member(x)  member(y)}

     x y {father(x,(g(x))  father((g(x),y) 

    grandfather(x,y)}
     bird(M)  fly(M)
    Step7: Move all universal quantifiers to the left
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x {married(x,f(x))  member(x)  member(y)}

     x y {father(x,(g(x))  father((g(x),y) 

    grandfather(x,y)}
     bird(M)  fly(M)
    Step8: Distribute  over 
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x {married(x,f(x))  member(x)  member(y)}

     x y {father(x,(g(x))  father((g(x),y) 

    grandfather(x,y)}
     bird(M)  fly(M)
    Step9: Simplify (Optional)
     x y z {Gaul(x)  Potion(y) 
    Hostile(z)  Sells(x,y,z)  Criminal(x)}
     x {married(x,f(x))  member(x)  member(y)}

     x y {father(x,(g(x))  father((g(x),y) 

    grandfather(x,y)}
     bird(M)  fly(M)

    You might also like