Question? Leave a message!

First-Order Logic

First-Order Logic
Dr.BenjaminClark Profile Pic
Dr.BenjaminClark,United States,Teacher
Published Date:21-07-2017
Website URL
First-Order Logic www.ThesisScientist.comLimitations of propositional logic • So far we studied propositional logic • Some English statements are hard to model in propositional logic: • “If your roommate is wet because of rain, your roommate must not be carrying any umbrella” • Pathetic attempt at modeling this: • RoommateWetBecauseOfRain = (NOT(RoommateCarryingUmbrella0) AND NOT(RoommateCarryingUmbrella1) AND NOT(RoommateCarryingUmbrella2) AND …) www.ThesisScientist.comProblems with propositional logic • No notion of objects • No notion of relations among objects • RoommateCarryingUmbrella0 is instructive to us, suggesting – there is an object we call Roommate, – there is an object we call Umbrella0, – there is a relationship Carrying between these two objects • Formally, none of this meaning is there – Might as well have replaced RoommateCarryingUmbrella0 by P www.ThesisScientist.comElements of first-order logic • Objects: can give these names such as Umbrella0, Person0, John, Earth, … • Relations: Carrying(., .), IsAnUmbrella(.) – Carrying(Person0, Umbrella0), IsUmbrella(Umbrella0) – Relations with one object = unary relations = properties • Functions: Roommate(.) – Roommate(Person0) • Equality: Roommate(Person0) = Person1 www.ThesisScientist.comThings to note about functions • It could be that we have a separate name for Roommate(Person0) • E.g., Roommate(Person0) = Person1 • … but we do not need to have such a name • A function can be applied to any object • E.g., Roommate(Umbrella0) www.ThesisScientist.comReasoning about many objects at once • Variables: x, y, z, … can refer to multiple objects • New operators “for all” and “there exists” – Universal quantifier and existential quantifier • for all x: CompletelyWhite(x) = NOT(PartiallyBlack(x)) – Completely white objects are never partially black • there exists x: PartiallyWhite(x) AND PartiallyBlack(x) – There exists some object in the world that is partially white and partially black www.ThesisScientist.comPractice converting English to first-order logic • “John has Jane’s umbrella” • Has(John, Umbrella(Jane)) • “John has an umbrella” • there exists y: (Has(John, y) AND IsUmbrella(y)) • “Anything that has an umbrella is not wet” • for all x: ((there exists y: (Has(x, y) AND IsUmbrella(y))) = NOT(IsWet(x))) • “Any person who has an umbrella is not wet” • for all x: (IsPerson(x) = ((there exists y: (Has(x, y) AND IsUmbrella(y))) = NOT(IsWet(x)))) www.ThesisScientist.comMore practice converting English to first-order logic • “John has at least two umbrellas” • there exists x: (there exists y: (Has(John, x) AND IsUmbrella(x) AND Has(John, y) AND IsUmbrella(y) AND NOT(x=y)) • “John has at most two umbrellas” • for all x, y, z: ((Has(John, x) AND IsUmbrella(x) AND Has(John, y) AND IsUmbrella(y) AND Has(John, z) AND IsUmbrella(z)) = (x=y OR x=z OR y=z)) www.ThesisScientist.comEven more practice converting English to first-order logic… • “Duke’s basketball team defeats any other basketball team” • for all x: ((IsBasketballTeam(x) AND NOT(x=BasketballTeamOf(Duke))) = Defeats(BasketballTeamOf(Duke), x)) • “Every team defeats some other team” • for all x: (IsTeam(x) = (there exists y: (IsTeam(y) AND NOT(x=y) AND Defeats(x,y))))More realistically… • “Any basketball team that defeats Duke’s basketball team in one year will be defeated by Duke’s basketball team in a future year” • for all x,y: (IsBasketballTeam(x) AND IsYear(y) AND DefeatsIn(x, BasketballTeamOf(Duke), y)) = there exists z: (IsYear(z) AND IsLaterThan(z,y) AND DefeatsIn(BasketballTeamOf(Duke), x, z)) www.ThesisScientist.comIs this a tautology? • “Property P implies property Q, or propery P implies property Q (or both)” • for all x: ((P(x) = Q(x)) OR (Q(x) = P(x))) • (for all x: (P(x) = Q(x)) OR (for all x: (Q(x) = P(x))) www.ThesisScientist.comRelationship between universal and existential • for all x: a • is equivalent to • NOT(there exists x: NOT(a)) www.ThesisScientist.comSomething we cannot do in first-order logic • We are not allowed to reason in general about relations and functions • The following would correspond to higher-order logic (which is more powerful): • “If John is Jack’s roommate, then any property of John is also a property of Jack’s roommate” • (John=Roommate(Jack)) = for all p: (p(John) = p(Roommate(Jack))) • “If a property is inherited by children, then for any thing, if that property is true of it, it must also be true for any child of it” • for all p: (IsInheritedByChildren(p) = (for all x, y: ((IsChildOf(x,y) AND p(y)) = p(x)))) www.ThesisScientist.comAxioms and theorems • Axioms: basic facts about the domain, our “initial” knowledge base • Theorems: statements that are logically derived from axioms www.ThesisScientist.comSUBST • SUBST replaces one or more variables with something else • For example: – SUBST(x/John, IsHealthy(x) = NOT(HasACold(x))) gives us – IsHealthy(John) = NOT(HasACold(John)) www.ThesisScientist.comInstantiating quantifiers • From • for all x: a • we can obtain • SUBST(x/g, a) • From • there exists x: a • we can obtain • SUBST(x/k, a) • where k is a constant that does not appear elsewhere in the knowledge base (Skolem constant) • Don’t need original sentence anymoreInstantiating existentials after universals • for all x: there exists y: IsParentOf(y,x) • WRONG: for all x: IsParentOf(k, x) • RIGHT: for all x: IsParentOf(k(x), x) • Introduces a new function (Skolem function) • … again, assuming k has not been used previously www.ThesisScientist.comGeneralized modus ponens • for all x: Loves(John, x) – John loves every thing • for all y: (Loves(y, Jane) = FeelsAppreciatedBy(Jane, y)) – Jane feels appreciated by every thing that loves her • Can infer from this: • FeelsAppreciatedBy(Jane, John) • Here, we used the substitution x/Jane, y/John – Note we used different variables for the different sentences • General UNIFY algorithms for finding a good substitution www.ThesisScientist.comKeeping things as general as possible in unification • Consider EdibleByWith – e.g., EdibleByWith(Soup, John, Spoon) – John can eat soup with a spoon • for all x: for all y: EdibleByWith(Bread, x, y) – Anything can eat bread with anything • for all u: for all v: (EdibleByWith(u, v, Spoon) = CanBeServedInBowlTo(u,v)) – Anything that is edible with a spoon by something can be served in a bowl to that something • Substitution: x/z, y/Spoon, u/Bread, v/z • Gives: for all z: CanBeServedInBowlTo(Bread, z) • Alternative substitution x/John, y/Spoon, u/Bread, v/John would only have given CanBeServedInBowlTo(Bread, John), which is not as generalResolution for first-order logic • for all x: (NOT(Knows(John, x)) OR IsMean(x) OR Loves(John, x)) – John loves everything he knows, with the possible exception of mean things • for all y: (Loves(Jane, y) OR Knows(y, Jane)) – Jane loves everything that does not know her • What can we unify? What can we conclude? • Use the substitution: x/Jane, y/John • Get: IsMean(Jane) OR Loves(John, Jane) OR Loves(Jane, John) • Complete (i.e., if not satisfiable, will find a proof of this), if we can remove literals that are duplicates after unification – Also need to put everything in canonical form first