Inference in First Order Logic课件.pptVIP

Inference in First Order Logic Some material adopted from notes by Tim Finin, Andreas Geyer-Schulz, and Chuck Dyer Inference Rules for FOL Inference rules for PL apply to FOL as well (Modus Ponens, And-Introduction, And-Elimination, etc.) New (sound) inference rules for use with quantifiers: Universal Elimination Existential Introduction Existential Elimination Generalized Modus Ponens (GMP) Resolution Clause form (CNF in FOL) Unification (consistent variable substitution) Refutation resolution (proof by contradiction) Universal Elimination (?x) P(x) |– P(c). If (?x) P(x) is true, then P(c) is true for any constant c in the domain of x, i.e., (?x) P(x) |= P(c). Replace all occurrences of x in the scope of ?x by the same ground term (a constant or a ground function). Example: (?x) eats(Ziggy, x) |– eats(Ziggy, IceCream) Existential Introduction P(c) |– (?x) P(x) If P(c) is true, so is (?x) P(x), i.e., P(c) |= (?x) P(x) Replace all instances of the given constant symbol by the same new variable symbol. Example eats(Ziggy, IceCream) |– (?x) eats(Ziggy, x) Existential Elimination From (?x) P(x) infer P(c), i.e., (?x) P(x) |= P(c), where c is a new constant symbol, All we know is there must be some constant that makes this true, so we can introduce a brand new one to stand in for that constant, even though we don’t know exactly what that constant refer to. Example: (?x) eats(Ziggy, x) |= eats(Ziggy, Stuff) Things become more complicated when there are universal quantifiers (?x)(?y) eats(x, y) |= (?x)eats(x, Stuff) ??? (?x)(?y) eats(x, y) |= eats(Ziggy, Stuff) ??? Introduce a new function food_sk(x) to stand for ?y because that y depends on x (?x)(?y) eats(x, y) |– (?x)eats(x, food_sk(x)) (?x)(?y) eats(x, y) |– eats(Ziggy, food_sk(Ziggy)) What exactly the function food_sk(.) does is unknown, except that it takes x as its argument The process of existential elimination is called “Skolemization”, and the new, unique constant