# INFO282 FOL

 John likes Mary or Jack, but not both (Likes(john, mary) ∨ Likes(john, jack)) ∧ ¬(Likes(john, mary)∧Likes(john,jack)) Mary likes someone who doesn’t like her. ∃x.(Likes(mary,x) ∧ ¬Likes(x,mary)) Tom dislikes anyone that Jack Likes ∀x.(Likes(jack,x) ⊃ ¬Likes(Tom,x)) Mary likes anyone who likes the same people as her ∀x.∀y.( (Likes(mary, y) ≡ Likes(x,y)) ⊃ Likes(mary,x)) For any two people, if one only loves himself then the other won’t love him. ∀x.∀y.((Loves(y, y) ∧ ∀z.(Loves(y, z) ⊃ z = y)) ⊃ ¬Loves(x, y) There are no two people where one loves the other, but the other loves herself only ¬∃x.∃y.((Loves(x, y) ∧ Loves(y, y) ∧ ∀z.(Loves(y, z) ⊃ z = y)) Nobody likes those who only like themselves ∀x.((Likes(x, x) ∧ ∀y.(Likes(x, y) ⊃ x = y)) ⊃ ¬∃z.(Likes(z, x)) Abbreviations (a ⊃ B) (a ≡ B) t1 ≠ t2 (a ⊃ B) is shorthand for (¬a ∨ B) ‘implication’ (a ≡ B) is shorthand for ((a ⊃ B) ∧ (B ⊃ a)) ‘equivalence’ t1 ≠ t2 is shorthand for ¬t1 = t2 ∧, ∨ ∧ and, ∨ or Stephen and Tom are good guys and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die G(s) ^ G(t)KB = {[G(s)], [G(t)]} Roger will shoot either Stephen or Tom and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die S(r,s) ∨ S(r,t)KB = {[S(r,s), S(r,t)]} Anyone who gets shot will die and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die ∀x((∃y.S(y,x)) ⊃ D(x))KB = {[¬S(y,x), D(x)]} Anyone who shoots a good guy will die and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die ∀x.∀y(S(x,y) ∧G(y) ⊃ D(x))KB = {[¬S(x,y), ¬G(y), ¬D(x)]} Roger will die and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die D(r) Some good guy will die and clause form in the following we use the following non-logical symbols: r = Roger, s = Stephen, t = Tom S(x,y) = x shoots y G(x) = x is a good guy D(x) = x will die ∃z.(G(z)∧D(z)) One of Henri or Pierre is a truth teller, and one is not. (Truth_teller(Henri) ∧  ¬Truth_teller(Pierre)) ∨  (¬Truth_teller(Henri) ∧  Truth_teller(Pierre)) An inhabitant will answer yes to a question if and only if he is a truth teller and the correct answer is yes, or he is not a truth teller and the correct answer is not yes. P only if Q P -> Q Answer_yes(x, q) -> ((Truth_teller(x) ∧  True(q)) ∨  (¬Truth_teller(x) ∧  ¬True(q))) The gauche question is correctly answered yes if and only if the proper direction is to go is left. True(gauche) -> Go_left A dit-oui (x , q ) question is correctly answered yes if and only if x will answer yes to question q. True(dit-oui (x, q)) -> Answer_yes(x, q) Show that there is a ground term t such that KB |= [Answer_yes (henri, t ) ≡  Go_left] T = ¬Answer_yes(pierre, Go_left) Would Henri answer Yes if I asked him if Pierre would not answer yes (no) to go left? q(x, q(x, q)) Answer_yes (henri, (¬Answer_yes(pierre, Go_left)) ) ≡  Go_left Suppose we have: Constants: 0 and 1 2-ary function symbol: + 2-ary predicate symbol: < and > Construct a model for S. ∀x. x > 0 ∀x. ∀y. (x < y ⊃ y > x) ∀x. ∀y. ∀z.((x < y ∧ y < z) ⊃ x < z)) T = D = {0, 1}I(>) = { <0,0>, <1,1> }I(<) = { <0,0>, <1,1>} 1. ∀x. x > 0>(0,0), >(1,1) true2. ∀x. ∀y. (x < y ⊃ y > x)<(0,0) ⊃ >(0,0) eller <(1,1) ⊃ >(1,1) true3. ∀x. ∀y. ∀z.((x < y ∧ y < z) ⊃ x < z))(0, 0) ∧ (0, 0) ⊃ (0, 0) true eller (1, 1) ∧ (1, 1) ⊃ (1, 1) true Formal proof How to change this {∀x.(𝛂(x) ⊃¬𝛃(x))} KB |= (𝛂(x) ⊃¬𝛃(x))KB |= ¬𝛂(x) V ¬¬𝛃(x)KB |= ¬𝛂(x) V 𝛃(x) KB: Is there a green block on top of a non-green block? a green, c is not, b is ? KB = On(a,b), On(b,c), Green(a), ¬Green(c) KB is the explicit knowledge representing the situation. Is ∃x.∃y.(Green(x) ∧ ¬Green(y) ∧ On(x,y)) implicit knowledge? PROOF: Is there a green block on top of a non-green block? a green, c is not, b is ? KB = On(a,b), On(b,c), Green(a), ¬Green(c) Given I |= Green(b) and I |= KBI |= Green(b) ∧ ¬Green(c) ∧ On(b,c)where x;b y;c∃x.∃y.(Green(x) ∧ ¬Green(y) ∧ On(x,y)) Given I |= ¬Green(b)I |= Green(a) ∧¬Green(b) ∧ On(a,b)where x;a y;b∃x.∃y.(Green(x) ∧ ¬Green(y) ∧ On(x,y)) distribute disjunctions convert to CNF P ∨ (Q ∧ R) (Q ∧ R) ∨ P (P∨Q) ∧ (P∨R)(Q∨P) ∧ (R∨P) Simplify Convert to CNF r → s ¬w → t (¬r ∨ s)(w ∨ t) Move negations in Convert to CNF ¬∀x P ¬∃x P ¬(P∧Q) ¬(P∨Q) ¬¬P ¬∀x P ≡ ∃x ¬P¬∃x P ≡ ∀x ¬P¬(P∧Q) ≡ (¬P∨¬Q)¬(P∨Q) ≡ (¬P∧¬Q)¬¬P ≡ P Skolemize Every philosopher writes at least one book ∀x[¬Philo(x) ∨ ∃y[Book(y) ∧ Write(x, y)]] Skolemize: substitute y by g(x)∀x[¬Philo(x) ∨ [Book(g(x)) ∧ Write(x, g(x))]] Skolemize ∀x∀y[¬Philo(x) ∨ ¬StudentOf (y, x) ∨ ∃z[Book(z) ∧ Write(x, z) ∧ Read(y, z)]] Skolemize: substitute z by h(x, y)∀x∀y[¬Philo(x) ∨ ¬StudentOf (y, x) ∨ [Book(h(x, y)) ∧ Write(x, h(x, y)) ∧ Read(y, h(x, y))]] Formal Proof Prove S∨{a}|= B  iff  S |=(a->b) S∨{a}|= B1.KB|=S∨{a}2.KB|=b3.KB|=Sfrom 1(((we have S or {a}, which means that if we allow S in our KB, then we have to have ¬a as well)))4.KB|=¬a ∧ bfrom 25.KB|=a->bfrom 46.S|= a->bfrom 3+5........................S|= a->b1.KB|=S2.KB|=a->b3.KB|=S∨{a}from14.KB|=afrom 35.KB|=bfrom 4+26.S∨{a}|= Bfrom 3+5 “If no man is blackmailing John, then is he being blackmailed by someone he loves?” ∀x[Man(x) ⊃ ¬Blackmails(x, john)] ⊃∃y [Loves(john, y) ∧ Blackmails(y, john)]? CNF Transformation with quantifiers Every formula is equivalent to some formula on CNF Eliminate the abbreviations ⊃ and ≡Push ¬ inwards so as to occur only in literals(Standardize variables. Rename quantified variables using equivalences such that all quantifiers have distinct variables.Eliminate all ∃Move all ∀ outward to include ∨ and  ∧ into their scopes)Distribute ∧ over ∨ Collapse CNF Eliminate the abbreviations ⊃ and ≡ expand a ≡ b to (a⊃b)∧(b⊃a)expand a⊃b to (¬a)∨bexpand b⊃c to (¬b)∨a CNF Push ¬ inwards so as to occur only in literals ¬(¬a) ≡ a¬(a∧b) ≡ ((¬a)∨(¬b))¬(a∨b) ≡ ((¬a)∧(¬b)) CNF Distribute ∧ over ∨ (a∨(b∧y)) ≡ ((a∨b)∧(a∨y))((b∧y)∨a) ≡ ((a∨b)∧(a∨y)) CNF Collapse (a∨a) ≡ a(a∧a) ≡ a CNF expand ≡ p≡(q⊃r) a ≡ b to (a⊃b)∧(b⊃a)expand ≡(p⊃(q⊃r)) ∧ ((q⊃r)⊃p) CNF expand ⊃ (p⊃(q⊃r)) ∧ ((q⊃r)⊃p) a⊃b to (¬a)∨bexpand ⊃((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p) CNF expand ⊃ ((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p) a⊃b to (¬a)∨bexpand ⊃((¬p)∨((¬q)∨r)) ∧ ((¬((¬q)∨r))∨p) CNF push negative ((¬p)∨((¬q)∨r)) ∧ ((¬((¬q)∨r))∨p) push¬((¬p)∨(¬q)∨r) ∧ (((¬(¬q))∧(¬r))∨p) CNF eliminate double ((¬p)∨(¬q)∨r) ∧ (((¬(¬q))∧(¬r))∨p) eliminate double ¬((¬p)∨(¬q)∨r) ∧ ((q∧(¬r))∨p) CNF distribute ((¬p)∨(¬q)∨r) ∧ ((q∧(¬r))∨p) distribute ∧ over ∨((¬p)∨(¬q)∨r) ∧ (q∨p) ∧ ((¬r) ∨p) Change this CNF formula to its clausal form and unit clauses ((¬p)∨(¬q)∨r) ∧ (q∨p) ∧ ((¬r) ∨p) clausal form{[¬p, ¬q, r], [q, p], [¬r, p]}unit clauses[p],[¬q] Interpretation of {} and [] C conjunction ∧ L disjunction ∨ Disjunction of no possibilities[] = ∨L = ¬TRUEConjunction of no constraints{} = ∧C = TRUEConjunction of False{[]} = ∧C = ¬TRUE C = {[p, q], [¬p, a, b], [¬p,c],[d,e]} C•p={[a,b],[c],[d,e]}C•¬p={[q],[d,e]} The Davis-Putnam Algorithm KB ∣=a iff KB∪{¬a} is unsatisfiable KB to Clause form Toddler Toddler ⊃ Child (Child ∧ Male) ⊃ Boy Infant ⊃ Child (Child ∧ Female) ⊃ Girl Female What is the notation for ∨ and ∧ [Toddler][¬Toddler, Child][¬Child, ¬Male, Boy][¬Infant, Child][¬Child, ¬Female, Girl][Female] ∨ = []∧ = , Is Alex a girl knowing she is a toddler and a female? [Toddler] [¬Toddler, Child] [¬Child, ¬Male, Boy] [¬Infant, Child] [¬Child, ¬Female, Girl] [Female] check from ¬Girl When there are no free occurrences of x in a, the following holds true: ∀y.a ∃y.a a ∧ ∀x.b (∀x.b) ∧ a a ∨ ∀x.b (∀x.b) ∨ a ∀y.a ≡ ∀x.a y/x∃y.a ≡ ∃x.a y/xa ∧ ∀x.b ≡ ∀x.(a∧b)(∀x.b) ∧ a ≡ ∀x.(a∧b)a ∨ ∀x.b ≡ ∀x.(a∨b)(∀x.b) ∨ a ≡ ∀x.(a∨b)        P or Q but not both (P ∧ ¬Q) ∨ (¬P ∧ Q) Every rich man loves jane Ax.((Man(x) ^ Rich(x)) -> Loves(x, jane)) All woman love john, except perhaps jane. Ax.((Woman(x) ^ x≠jane) -> Loves(x,john)) No one blackmails the ones they love Ax.Ay.(Loves(x,y) -> ¬Blackmails(x,y)) Authorburntoutmatch ID336702 Card SetINFO282 FOL Descriptionexam prep Updated2018-02-22T17:38:03Z Show Answers