First-Order Logic (FOL) aka. predicate calculusFirst-Order Logic (FOL) SyntaxFirst-Order Logic (FOL) Syntax…QuantifiersQuantifiers …Slide 6Translating English to FOLTranslating English to FOL…Inference Rules for FOLSlide 10Slide 11Automated Inference in FOLIncompleteness of the generalized modus ponens inference ruleGeneralized Modus Ponens in Horn FOLExample of forward chainingBackward chainingResolution Procedure (aka Resolution Refutation Procedure)Resolution Procedure…UnificationUnification AlgorithmUnification…Slide 22Slide 23Resolution AlgorithmResolution example (using PL sentences)Resolution example (using PL sentences)…Problems yet to be addressedConverting FOL sentences to clause formConverting FOL sentences to clause form…Slide 30Slide 31Slide 32Slide 33Example: Hoofers Club [example from Charles Dyer]Example: Hoofers Club…Slide 36Slide 37Slide 38Resolution procedure as searchSome strategies for controlling resolution's searchSubsumptionFirst-Order Logic (FOL)aka. predicate calculusTuomas SandholmCarnegie Mellon UniversityComputer Science DepartmentFirst-Order Logic (FOL) Syntax•User defines these primitives: –Constant symbols (i.e., the "individuals" in the world) E.g., Mary, 3 –Function symbols (mapping individuals to individuals) E.g., father-of(Mary) = John, color-of(Sky) = Blue –Predicate symbols (mapping from individuals to truth values) E.g., greater(5,3), green(Grass), color(Grass, Green)First-Order Logic (FOL) Syntax…•FOL supplies these primitives: –Variable symbols. E.g., x,y –Connectives. Same as in PL: not (~), and (^), or (v), implies (=>), if and only if (<=>) –Quantifiers: Universal (A) and Existential (E)Quantifiers•Universal quantification corresponds to conjunction ("and") in that (Ax)P(x) means that P holds for all values of x in the domain associated with that variable. –E.g., (Ax) dolphin(x) => mammal(x) •Existential quantification corresponds to disjunction ("or") in that (Ex)P(x) means that P holds for some value of x in the domain associated with that variable. –E.g., (Ex) mammal(x) ^ lays-eggs(x) •Universal quantifiers are usually used with "implies" to form "if-then rules." –E.g., (Ax) cs15-381-student(x) => smart(x) means "All cs15-381 students are smart." –You rarely use universal quantification to make blanket statements about every individual in the world: (Ax)cs15-381-student(x) ^ smart(x) meaning that everyone in the world is a cs15-381 student and is smart.Quantifiers …•Existential quantifiers are usually used with "and" to specify a list of properties or facts about an individual. –E.g., (Ex) cs15-381-student(x) ^ smart(x) means "there is a cs15-381 student who is smart." –A common mistake is to represent this English sentence as the FOL sentence: (Ex) cs15-381-student(x) => smart(x) •Switching the order of universal quantifiers does not change the meaning: (Ax)(Ay)P(x,y) is logically equivalent to (Ay)(Ax)P(x,y). Similarly, you can switch the order of existential quantifiers. •Switching the order of universals and existentials does change meaning: –Everyone likes someone: (Ax)(Ey)likes(x,y) –Someone is liked by everyone: (Ey)(Ax)likes(x,y)First-Order Logic (FOL) Syntax…•Sentences are built up of terms and atoms: –A term (denoting a real-world object) is a constant symbol, a variable symbol, or a function e.g. left-leg-of ( ). For example, x and f(x1, ..., xn) are terms, where each xi is a term. –An atom (which has value true or false) is either an n-place predicate of n terms, or, if P and Q are atoms, then ~P, P V Q, P ^ Q, P => Q, P <=> Q are atoms –A sentence is an atom, or, if P is a sentence and x is a variable, then (Ax)P and (Ex)P are sentences –A well-formed formula (wff) is a sentence containing no "free" variables. I.e., all variables are "bound" by universal or existential quantifiers. •E.g., (Ax)P(x,y) has x bound as a universally quantified variable, but y is free.Translating English to FOL•Every gardener likes the sun.(Ax) gardener(x) => likes(x,Sun) •You can fool some of the people all of the time.(Ex)(At) (person(x) ^ time(t)) => can-fool(x,t) •You can fool all of the people some of the time.(Ax)(Et) (person(x) ^ time(t) => can-fool(x,t) •All purple mushrooms are poisonous.(Ax) (mushroom(x) ^ purple(x)) => poisonous(x)Translating English to FOL…•No purple mushroom is poisonous.~(Ex) purple(x) ^ mushroom(x) ^ poisonous(x) or, equivalently,(Ax) (mushroom(x) ^ purple(x)) => ~poisonous(x) •There are exactly two purple mushrooms.(Ex)(Ey) mushroom(x) ^ purple(x) ^ mushroom(y) ^ purple(y) ^ ~(x=y) ^ (Az) (mushroom(z) ^ purple(z)) => ((x=z) v (y=z))•Deb is not tall.~tall(Deb) •X is above Y if X is on directly on top of Y or else there is a pile of one or more other objects directly on top of one another starting with X and ending with Y.(Ax)(Ay) above(x,y) <=> (on(x,y) v (Ez) (on(x,z) ^ above(z,y)))Inference Rules for FOL•Inference rules for PL apply to FOL as well. For example, Modus Ponens, And-Introduction, And-Elimination, etc. •New sound inference rules for use with quantifiers: –Universal EliminationIf (Ax)P(x) is true, then P(c) is true, where c is a constant in the domain of x. For example, from (Ax)eats(Ziggy, x) we can infer eats(Ziggy, IceCream). •The variable symbol can be replaced by any ground term, i.e., any constant symbol or function symbol applied to ground terms only. –Existential IntroductionIf P(c) is true, then (Ex)P(x) is inferred. •For example, from eats(Ziggy, IceCream) we can infer (Ex)eats(Ziggy, x). •All instances of the given constant symbol are replaced by the new variable symbol. Note that the variable symbol cannot already exist anywhere in the expression. –Existential EliminationFrom (Ex)P(x) infer P(c). •For example, from (Ex)eats(Ziggy, x) infer eats(Ziggy, Cheese). •Note that the variable is replaced by a brand new constant that does not occur in this or any other sentence in the Knowledge Base. In other words, we don't want to accidentally draw other inferences about it by introducing the constant. 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 (unknown) constant.Inference Rules for FOL•Paramodulation–Given two sentences (P1 v ... v PN) and (t=s v Q1 v ... v QM) where each Pi and Qi is a literal and Pj contains a term t, derive new sentence (P1 v ... v Pj-1 v Pj[s] v Pj+1 v ... v PN v Q1
View Full Document
Unlocking...