INFO282 FOL

  1. John likes Mary or Jack, but not both
    (Likes(john, mary) ∨ Likes(john, jack)) ∧ ¬(Likes(john, mary)∧Likes(john,jack))
  2. Mary likes someone who doesn’t like her.
    ∃x.(Likes(mary,x) ∧ ¬Likes(x,mary))
  3. Tom dislikes anyone that Jack Likes
    ∀x.(Likes(jack,x) ⊃ ¬Likes(Tom,x))
  4. Mary likes anyone who likes the same people as her
    ∀x.∀y.( (Likes(mary, y) ≡ Likes(x,y)) ⊃ Likes(mary,x))
  5. 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)
  6. 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))
  7. Nobody likes those who only like themselves
    ∀x.((Likes(x, x) ∧ ∀y.(Likes(x, y) ⊃ x = y)) ⊃ ¬∃z.(Likes(z, x))
  8. 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
  9. ∧, ∨
    ∧ and, ∨ or
  10. 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)]}
  11. 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)]}
  12. 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)]}
  13. 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)]}
  14. 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)
  15. 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))
  16. 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))
  17. 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)))
  18. The gauche question is correctly answered yes if and only if the proper direction is to go is left.
    True(gauche) -> Go_left
  19. 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)
  20. Show that there is a ground term t such that KB |= [Answer_yes (henri, t ) ≡  Go_left]
    T = ¬Answer_yes(pierre, Go_left)
  21. 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
  22. 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,I>
    • D = {0, 1}
    • I(>) = { <0,0>, <1,1> }
    • I(<) = { <0,0>, <1,1>}

    • 1. ∀x. x > 0
    • >(0,0), >(1,1) true
    • 2. ∀x. ∀y. (x < y ⊃ y > x)
    • <(0,0) ⊃ >(0,0) eller <(1,1) ⊃ >(1,1) true
    • 3. ∀x. ∀y. ∀z.((x < y ∧ y < z) ⊃ x < z))
    • (0, 0) ∧ (0, 0) ⊃ (0, 0) true eller (1, 1) ∧ (1, 1) ⊃ (1, 1) true
  23. Formal proof
    How to change this
    {∀x.(𝛂(x) ⊃¬𝛃(x))}
    • KB |= (𝛂(x) ⊃¬𝛃(x))
    • KB |= ¬𝛂(x) V ¬¬𝛃(x)
    • KB |= ¬𝛂(x) V 𝛃(x)
  24. 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?
  25. 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 |= KB
    • I |= 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))
  26. distribute disjunctions
    convert to CNF
    P ∨ (Q ∧ R)
    (Q ∧ R) ∨ P
    • (P∨Q) ∧ (P∨R)
    • (Q∨P) ∧ (R∨P)
  27. Simplify
    Convert to CNF
    r → s
    ¬w → t
    • (¬r ∨ s)
    • (w ∨ t)
  28. 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
  29. 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))]]
  30. 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))]]
  31. Formal Proof
    Prove S∨{a}|= B  iff  S |=(a->b)
    • S∨{a}|= B
    • 1.KB|=S∨{a}
    • 2.KB|=b
    • 3.KB|=S
    • from 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 ∧ b
    • from 2
    • 5.KB|=a->b
    • from 4
    • 6.S|= a->b
    • from 3+5
    • ........................
    • S|= a->b
    • 1.KB|=S
    • 2.KB|=a->b
    • 3.KB|=S∨{a}
    • from1
    • 4.KB|=a
    • from 3
    • 5.KB|=b
    • from 4+2
    • 6.S∨{a}|= B
    • from 3+5
  32. “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)]?
  33. 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
  34. CNF
    Eliminate the abbreviations ⊃ and ≡
    • expand a ≡ b to (a⊃b)∧(b⊃a)
    • expand a⊃b to (¬a)∨b
    • expand b⊃c to (¬b)∨a
  35. CNF
    Push ¬ inwards so as to occur only in literals
    • ¬(¬a) ≡ a
    • ¬(a∧b) ≡ ((¬a)∨(¬b))
    • ¬(a∨b) ≡ ((¬a)∧(¬b))
  36. CNF
    Distribute ∧ over ∨
    • (a∨(b∧y)) ≡ ((a∨b)∧(a∨y))
    • ((b∧y)∨a) ≡ ((a∨b)∧(a∨y))
  37. CNF
    Collapse
    • (a∨a) ≡ a
    • (a∧a) ≡ a
  38. CNF expand ≡
    p≡(q⊃r)
    • a ≡ b to (a⊃b)∧(b⊃a)
    • expand ≡
    • (p⊃(q⊃r)) ∧ ((q⊃r)⊃p)
  39. CNF expand ⊃
    (p⊃(q⊃r)) ∧ ((q⊃r)⊃p)
    • a⊃b to (¬a)∨b
    • expand ⊃
    • ((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p)
  40. CNF expand ⊃
    ((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p)
    • a⊃b to (¬a)∨b
    • expand ⊃
    • ((¬p)∨((¬q)∨r)) ∧ ((¬((¬q)∨r))∨p)
  41. CNF push negative
    ((¬p)∨((¬q)∨r)) ∧ ((¬((¬q)∨r))∨p)
    • push¬
    • ((¬p)∨(¬q)∨r) ∧ (((¬(¬q))∧(¬r))∨p)
  42. CNF eliminate double
    ((¬p)∨(¬q)∨r) ∧ (((¬(¬q))∧(¬r))∨p)
    • eliminate double ¬
    • ((¬p)∨(¬q)∨r) ∧ ((q∧(¬r))∨p)
  43. CNF distribute
    ((¬p)∨(¬q)∨r) ∧ ((q∧(¬r))∨p)
    • distribute ∧ over ∨
    • ((¬p)∨(¬q)∨r) ∧ (q∨p) ∧ ((¬r) ∨p)
  44. 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]
  45. Interpretation of {} and []
    C conjunction ∧
    L disjunction ∨
    • Disjunction of no possibilities
    • [] = ∨L = ¬TRUE
    • Conjunction of no constraints
    • {} = ∧C = TRUE
    • Conjunction of False
    • {[]} = ∧C = ¬TRUE
  46. C = {[p, q], [¬p, a, b], [¬p,c],[d,e]}
    • C•p={[a,b],[c],[d,e]}
    • C•¬p={[q],[d,e]}
  47. The Davis-Putnam Algorithm
    KB ∣=a iff KB∪{¬a} is unsatisfiable
  48. 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]

    • ∨ = []
    • ∧ = ,
  49. 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
    • Image Upload 1
  50. 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/x
    • a ∧ ∀x.b ≡ ∀x.(a∧b)
    • (∀x.b) ∧ a ≡ ∀x.(a∧b)
    • a ∨ ∀x.b ≡ ∀x.(a∨b)
    • (∀x.b) ∨ a ≡ ∀x.(a∨b)
  51. Image Upload 2
    Image Upload 3
  52. Image Upload 4
    Image Upload 5
  53. Image Upload 6
    Image Upload 7
  54. Image Upload 8
    Image Upload 9
  55. P or Q but not both
    (P ∧ ¬Q) ∨ (¬P ∧ Q)
  56. Every rich man loves jane
    Ax.((Man(x) ^ Rich(x)) -> Loves(x, jane))
  57. All woman love john, except perhaps jane.
    Ax.((Woman(x) ^ x≠jane) -> Loves(x,john))
  58. No one blackmails the ones they love
    Ax.Ay.(Loves(x,y) -> ¬Blackmails(x,y))
Author
burntoutmatch
ID
336702
Card Set
INFO282 FOL
Description
exam prep
Updated