Yioop - 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))

-- 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.

-- 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

∀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>∀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>