-
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
-
-
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,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
-
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 |= 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))
-
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
-
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}|= 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
-
“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)∨b
- expand 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 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)∨b
- expand ⊃
- ((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p)
-
CNF expand ⊃
((¬p)∨(q⊃r)) ∧ ((¬(q⊃r))∨p)
- a⊃b to (¬a)∨b
- expand ⊃
- ((¬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 = ¬TRUE
- Conjunction of no constraints
- {} = ∧C = TRUE
- Conjunction 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]
-
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)
-
-
-
-
-
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))
|
|