PHP Search Engine

Nov 9 In-Class Exercise Thread .

Please post your solutions to the Nov 9 In-Class Exercise to this thread.

Best,

Chris

Please post your solutions to the Nov 9 In-Class Exercise to this thread. Best, Chris

-- Nov 9 In-Class Exercise Thread

x [y Animal(y) Loves(x,y)] [y Loves(y,x)] (Starting statement)

x [y Animal(y)Loves(x,y)][y Loves(y,x)] (Eliminate implication)

x [y (Animal(y)Loves(x,y))][y Loves(y,x)] (Moving negation inward)

x [y Animal(y) Loves(x,y)][y Loves(y,x)] (De Morgan's Law)

x [y Animal(y) Loves(x,y)][y Loves(y,x)] (Double Negation equivalence)

x [y Animal(y) Loves(x,y)][z Loves(z,x)] (Standardize variables)

x [Animal(F(x)) Loves(x,F(x))]Loves(G(x),x) (Skolemization)

Animal(F(x)) Loves(x,F(x))]Loves(G(x),x) (Remove universal quantifiers)

[Animal(F(x))Loves(G(x),x)][Loves(x,F(x))Loves(G(x),x)] (Distributivity of and )

A1. Animal(F(x))Loves(G(x),x) A2. Loves(x,F(x))Loves(G(x),x)

E. Cat(Tuna) F. Cat(x) Animal(x)

Both E and F are terms. Therefore

we return

Unify(Tuna, x, Unify(Cat(a), Cat(a), ()) )

The second Unify would return the empty list.

Going back to the first Unify, y is a var, we call

Unify-var(x, Tuna, ())

This would append x with Tuna, so we have x | -> Tuna in S, giving us (x |-> Tuna)

(Edited: 2022-11-09)

∀x [∀y Animal(y) ⇒ Loves(x,y)] ⇒ [∃y Loves(y,x)] (Starting statement) ∀x ¬[∀y ¬Animal(y)∨Loves(x,y)]∨[∃y Loves(y,x)] (Eliminate implication) ∀x [∃y ¬(¬Animal(y)∨Loves(x,y))]∨[∃y Loves(y,x)] (Moving negation inward) ∀x [∃y ¬¬Animal(y)∧ ¬Loves(x,y)]∨[∃y Loves(y,x)] (De Morgan's Law) ∀x [∃y Animal(y)∧ ¬Loves(x,y)]∨[∃y Loves(y,x)] (Double Negation equivalence) ∀x [∃y Animal(y)∧ ¬Loves(x,y)]∨[∃z Loves(z,x)] (Standardize variables) ∀x [Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) (Skolemization) Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) (Remove universal quantifiers) [Animal(F(x))∨Loves(G(x),x)]∧[¬Loves(x,F(x))∨Loves(G(x),x)] (Distributivity of ∨ and ∧) A1. Animal(F(x))∨Loves(G(x),x) A2. ¬Loves(x,F(x))∨Loves(G(x),x) E. Cat(Tuna) F. ¬Cat(x) ∨ Animal(x) Both E and F are terms. Therefore we return Unify(Tuna, x, Unify(Cat(a), Cat(a), ()) ) The second Unify would return the empty list. Going back to the first Unify, y is a var, we call Unify-var(x, Tuna, ()) This would append x with Tuna, so we have x | -> Tuna in S, giving us (x |-> Tuna)

-- Nov 9 In-Class Exercise Thread

x [y Animal(y) => Loves(x, y)] => [y Loves(y, x)] x [y Animal(y) => Loves(x, y)] [y Loves(y, x)] x [y Animal(y) Loves(x, y)] [y Loves(y, x)] x [y Animal(y) Loves(x, y)] [y Loves(y, x)] x [Animal(F(x)) Loves(x, F(x))] [Loves(G(x), x)] (Animal(F(x)) Loves(G(x), x)) (Loves(x, F(x)) Loves(G(x), x))

∀x [∀y Animal(y) => Loves(x, y)] => [∃y Loves(y, x)] ∀x ¬[∀y Animal(y) => Loves(x, y)] ∨ [∃y Loves(y, x)] ∀x ¬[∀y ¬Animal(y) ∨ Loves(x, y)] ∨ [∃y Loves(y, x)] ∀x [∃y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃y Loves(y, x)] ∀x [Animal(F(x)) ∧ ¬Loves(x, F(x))] ∨ [Loves(G(x), x)] (Animal(F(x)) ∨ Loves(G(x), x)) ∧ (¬Loves(x, F(x)) ∨ Loves(G(x), x))

-- Nov 9 In-Class Exercise Thread

x(y(Animal(y)) => Loves(x, y)) => (y(Loves(y, x))) x(y(Animal(y)) => Loves(x, y)) (y(Loves(y, x))) x(y(Animal(y)) Loves(x, y)) (y(Loves(y, x))) x(y(Animal(y)) Loves(x, y)) (y(Loves(y, x))) x(Animal(F(x)) Loves(x, F(x))) (Loves(G(x), x)) (Animal(F(x)) Loves(G(x), x)) (Loves(x, F(x)) Loves(G(x), x))

∀x(∀y(Animal(y)) => Loves(x, y)) => (∃y(Loves(y, x))) ∀x¬(∀y(Animal(y)) => Loves(x, y)) ∨ (∃y(Loves(y, x))) ∀x¬(∀y¬(Animal(y)) ∨ Loves(x, y)) ∨ (∃y(Loves(y, x))) ∀x(∃y(Animal(y)) ∧ ¬Loves(x, y)) ∨ (∃y(Loves(y, x))) ∀x(Animal(F(x)) ∧ ¬Loves(x, F(x))) ∨ (Loves(G(x), x)) (Animal(F(x)) ∨ Loves(G(x), x)) ∧ (¬Loves(x, F(x)) ∨ Loves(G(x), x))

-- Nov 9 In-Class Exercise Thread

E. Cat (Tuna) F. x Cat(X)=> Animal(x) Unify (Tuna, x Unify( Cat(a), Cat(a), ())) We then go back to the first unify and call Unify-var(x, Tuna, ()) Then we get x|-> Tuna which we can then find a refutation for.

E. Cat (Tuna) F. ∀x Cat(X)=> Animal(x) Unify (Tuna, x Unify( Cat(a), Cat(a), ())) We then go back to the first unify and call Unify-var(x, Tuna, ()) Then we get x|-> Tuna which we can then find a refutation for.

-- Nov 9 In-Class Exercise Thread

x (y Animal(y) => Loves(x, y)) => (y Loves(y, x)) x not(y Animal(y) => Loves(x, y)) or (y Loves(y, x)) x not(y not Animal(y) or Loves(x, y)) or (y Loves(y, x)) x (y Animal(y) and not Loves(x, y)) or (y Loves(y, x)) x (Animal(F(x)) and not Loves(x, F(x))) or (Loves(G(x), x)) (Animal(F(x)) or Loves(G(x), x)) and (not Loves(x, F(x)) or Loves(G(x), x))

∀x (∀y Animal(y) => Loves(x, y)) => (∃y Loves(y, x)) ∀x not(∀y Animal(y) => Loves(x, y)) or (∃y Loves(y, x)) ∀x not(∀y not Animal(y) or Loves(x, y)) or (∃y Loves(y, x)) ∀x (∃y Animal(y) and not Loves(x, y)) or (∃y Loves(y, x)) ∀x (Animal(F(x)) and not Loves(x, F(x))) or (Loves(G(x), x)) (Animal(F(x)) or Loves(G(x), x)) and (not Loves(x, F(x)) or Loves(G(x), x))

-- Nov 9 In-Class Exercise Thread

A. x[y Animal(y) => Loves(x, y)] => [y Loves(y, x)] x[y Animal(y) Loves(x, y)] => [y Loves(y, x)] x [y Animal(y) Loves(x, y)] [y Loves(y, x)] x [y Animal(y) Loves(x, y)] [y Loves(y, x)] x [Animal(F(x)) Loves(x, F(x))] [y Loves(G(x), x)] [Animal(F(x)) Loves(G(x), x)] [Loves(x, F(x)) Loves(G(x), x)] '''Result:''' A1. Animal(F(x)) Loves(G(x), x) A2. Loves(x, F(x)) Loves(G(x), x)

E. Cat(Tuna) F. Cat(x) Animal(x) Since E and F are both terms, we return Unify (Tuna, x, Unify(Cat(a), Cat(a), S)) (a,b are new variable names, and S, the substitution list is ()) Unify-var (x, Tuna, S) x |-> Tuna Therefore, refutation can be applied.

(Edited: 2022-11-09)

A. ∀x[∀y Animal(y) => Loves(x, y)] => [∃y Loves(y, x)] ∀x[∀y ¬Animal(y) ∨ Loves(x, y)] => [∃y Loves(y, x)] ∀x ¬[∀y ¬Animal(y) ∨ Loves(x, y)] ∨ [∃y Loves(y, x)] ∀x [∀y Animal(y) ∧ ¬Loves(x, y)] ∨ [∃y Loves(y, x)] ∀x [Animal(F(x)) ∧ ¬Loves(x, F(x))] ∨ [∃y Loves(G(x), x)] [Animal(F(x)) ∨ Loves(G(x), x)] ∧ [¬Loves(x, F(x)) ∨ Loves(G(x), x)] '''Result:''' A1. Animal(F(x)) ∨ Loves(G(x), x) A2. ¬Loves(x, F(x)) ∨ Loves(G(x), x) E. Cat(Tuna) F. ¬Cat(x) ∨ Animal(x) Since E and F are both terms, we return Unify (Tuna, x, Unify(Cat(a), Cat(a), S)) (a,b are new variable names, and S, the substitution list is ()) Unify-var (x, Tuna, S) x |-> Tuna Therefore, refutation can be applied.

-- Nov 9 In-Class Exercise Thread

A. x [y Animal(y) Loves(x, y)] [y Loves(y, x)] x [y Animal(y)Loves(x, y)][y Loves(y, x)] x [y (Animal(y)Loves(x, y))][y Loves(y, x)] x [y Animal(y) Loves(x, y)][y Loves(y, x)] x [y Animal(y) Loves(x, y)][y Loves(y, x)] x [y Animal(y) Loves(x, y)][z Loves(z, x)] x [Animal(F(x)) Loves(x,F(x))]Loves(G(x),x) Animal(F(x)) Loves(x,F(x))]Loves(G(x),x) [Animal(F(x))Loves(G(x),x)][Loves(x,F(x))Loves(G(x),x)] A1. Animal(F(x))Loves(G(x),x) A2. Loves(x,F(x))Loves(G(x),x)

E. Cat(Tuna) F. Cat(x) Unify(Tuna, x, Unify(Cat(a), Cat(a), ()) ) Unify-var(x, Tuna, S) This would append x with Tuna, so we have x | -> Tuna in S

A. ∀x [∀y Animal(y) ⇒ Loves(x, y)] ⇒ [∃y Loves(y, x)] ∀x ¬[∀y ¬Animal(y)∨Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y ¬(¬Animal(y)∨Loves(x, y))]∨[∃y Loves(y, x)] ∀x [∃y ¬¬Animal(y)∧ ¬Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y Animal(y)∧ ¬Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y Animal(y)∧ ¬Loves(x, y)]∨[∃z Loves(z, x)] ∀x [Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) [Animal(F(x))∨Loves(G(x),x)]∧[¬Loves(x,F(x))∨Loves(G(x),x)] A1. Animal(F(x))∨Loves(G(x),x) A2. ¬Loves(x,F(x))∨Loves(G(x),x) E. Cat(Tuna) F. ¬Cat(x) Unify(Tuna, x, Unify(Cat(a), Cat(a), ()) ) Unify-var(x, Tuna, S) This would append x with Tuna, so we have x | -> Tuna in S

-- Nov 9 In-Class Exercise Thread

x [y Animal(y) Loves(x,y)] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [y Loves(y,x)] x [y (Animal(y) Loves(x,y))] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [y Loves(y,x)] x [y Animal(y) Loves(x,y)] [z Loves(z,x)] x [Animal(F(x)) Loves(x,F(x))] Loves(G(x),x) Animal(F(x)) Loves(x,F(x))] Loves(G(x),x) [Animal(F(x)) Loves(G(x),x)] [Loves(x,F(x)) Loves(G(x),x)]

(Edited: 2022-11-09)

∀x [∀y Animal(y) ⇒ Loves(x,y)] ⇒ [∃y Loves(y,x)] ∀x ¬[∀y ¬Animal(y) ∨ Loves(x,y)] ∨ [∃y Loves(y,x)] ∀x [∃y ¬(¬Animal(y) ∨ Loves(x,y))] ∨ [∃y Loves(y,x)] ∀x [∃y ¬¬Animal(y) ∧ ¬Loves(x,y)] ∨ [∃y Loves(y,x)] ∀x [∃y Animal(y) ∧ ¬Loves(x,y)] ∨ [∃y Loves(y,x)] ∀x [∃y Animal(y) ∧ ¬Loves(x,y)] ∨ [∃z Loves(z,x)] ∀x [Animal(F(x)) ∧ ¬Loves(x,F(x))] ∨ Loves(G(x),x) Animal(F(x)) ∧ ¬Loves(x,F(x))] ∨ Loves(G(x),x) [Animal(F(x)) ∨ Loves(G(x),x)] ∧ [¬Loves(x,F(x)) ∨ Loves(G(x),x)]

-- Nov 9 In-Class Exercise Thread

<nowiki>x [y Animal(y) Loves(x, y)] [y Loves(y, x)]

x [y Animal(y)Loves(x, y)][y Loves(y, x)]

x [y (Animal(y)Loves(x, y))][y Loves(y, x)]

x [y Animal(y) Loves(x, y)][y Loves(y, x)]

x [y Animal(y) Loves(x, y)][z Loves(z, x)]

x [Animal(F(x)) Loves(x,F(x))]Loves(G(x),x)

Animal(F(x)) Loves(x,F(x))]Loves(G(x),x)

[Animal(F(x))Loves(G(x),x)][Loves(x,F(x))Loves(G(x),x)]

E. Cat(Tuna)

F. not Cat(x) or Animal(x)

Unify(Tuna, x, ())

Unify(Tuna,x, Unify(Cat(a),Cat(a), ()))

Unify-var(x,Tuna,S)

(x |-> Tuna)</nowiki>

<nowiki>∀x [∀y Animal(y) ⇒ Loves(x, y)] ⇒ [∃y Loves(y, x)] ∀x ¬[∀y ¬Animal(y)∨Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y ¬(¬Animal(y)∨Loves(x, y))]∨[∃y Loves(y, x)] ∀x [∃y ¬¬Animal(y)∧ ¬Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y Animal(y)∧ ¬Loves(x, y)]∨[∃y Loves(y, x)] ∀x [∃y Animal(y)∧ ¬Loves(x, y)]∨[∃z Loves(z, x)] ∀x [Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) Animal(F(x))∧ ¬Loves(x,F(x))]∨Loves(G(x),x) [Animal(F(x))∨Loves(G(x),x)]∧[¬Loves(x,F(x))∨Loves(G(x),x)] E. Cat(Tuna) F. not Cat(x) or Animal(x) Unify(Tuna, x, ()) Unify(Tuna,x, Unify(Cat(a),Cat(a), ())) Unify-var(x,Tuna,S) (x |-> Tuna)</nowiki>