CSE 4308 / CSE 5360 - Artificial Intelligence I Homework 3: Logic InferenceCSE 4308 / CSE 5360 - Artificial Intelligence IHomework 3- Fall 2013Due Date: Oct. 15 2013, 12:30 pmProblems marked with a∗are required only for students in the graduate section(CSE 5360). They will be graded for extra credit for students of CSE 4308.Propositional Logic1. Translate the following facts into propositional logic sentences. Make sureyou list all the propositions and their meanings.a) Insects have six legs.b) If insects had eight legs they would be related to spiders.c) Animals that are related to Spiders are also related to Scorpions.d) If insects are six legged animals then they are not related to scorpions.2. Show that the following sentences follow from the given knowledge baseusing equivalence and inference rule. (Give all the steps of your proof andindicate what rule you used).KB : P ∧ QP ⇒ (R ∨ S)(A ∨ Q) ⇒ (P ⇒ S)¬((A ∧ S) ∨ (A ∧ P )) ∨ (Q ∧ R)A ∨ (¬P ∧ ¬Q)T RUE ⇒ (A ∧ (P ⇒ Q))V ∨ ¬P ∨ ¬Ua) P ∧ Ab) V ⇒ Sc)∗T RUE ⇒ Qd)∗(Q ∧ U ) ⇒ V2013 Manfred Huber Page 1CSE 4308 / CSE 5360 - Artificial Intelligence I Homework 3: Logic InferenceFirst-order Logic3. Translate the following facts into sentences in first-order logic.a) Dogs and cats eat meat.b) Every bottle that is filled contains liquid.c) Since Jim and Jack take the same classes, Jack works on the sameassignments as Jim.d) If Mary is John’s daughter then Mary is younger than John.4. Determine for each of the following pairs of sentences if they can be unifiedand if they can, give the most general unifier.a) (Aunt(x, y) ∧ ¬Man(x) ∨ Uncle(x, y))(Aunt(Mary, z) ∨ ¬M an(John) ∨ Uncle(v, z))b) ((F ather(x, Jack) ∧ Mother (y, Jack)) ⇒ Married(x, y))((F ather(y, z) ∧ M other(Mary, z)) ⇒ Married(y, M ary))c) ((Son(x, x)∧Sister(Mary, Jack)) ⇒ (Daughter(x, Mary)∧Brother(Jack, M ary)))((Son(Jack, x)∧Sister(z, x)) ⇒ (Daughter(z, f(x))∧Brother(y, z)))d) ((Married(x, y) ∧ F ather(x, Mary)) ⇒ Man(x))((Married(z, f(Jack)) ∨ F ather(z, v)) ⇒ Man(z))5. Transform the following sentences into conjunctive normal form.a) P (John) ⇒ ∃x(Q(x) ∧ R(John, x))b) ∀x(∃y(P (x) ∧ ¬Q(x, y) ∧ R(y))) ⇒ ∀y¬S(x, y))c) ¬(∃x∀y(P (x) ⇒ ∀yQ(y)) ∧ ∀zR(z))d)∗∃x(¬∀y(P (x, y) ⇒ Q(x)) ∧ ∀y(R(y) ⇒ ∃zP (y, z)))2013 Manfred Huber Page 2CSE 4308 / CSE 5360 - Artificial Intelligence I Homework 3: Logic Inference6. Use resolution with refutation to show that the following queries can be in-ferred from the given knowledge base. At each resolution step also indicatethe corresponding unifier.KB : F ather(J ohn, Jack)Married(John, J ane)Man(Jack)F ather(x1, y1) ⇒ Man(x1)Mother(x2, y2) ⇒ W oman(x2)Married(x3, y3) ∧ F ather(x3, z3) ⇒ Mother(y3, z3)F ather(x4, y4) ∧ M other(z4, y4) ⇒ Married(x4, z4) ∨ Divorced(x4)Divorced(John) ⇒ F alseMother(Mary, Jack)Married(x5, y5) ∧ Son(z5, x5) ⇒ Son(z5, y5)F ather(x6, y6) ∧ M an(y6) ⇒ Son(y6, x6)a) Married(John, M ary)b) W oman(Mary) ∧ W oman(Jane)c)∗Son(Jack, M ary) ∧ Son(J ack, J ane)7. Translate the knowledge base of problem 6 into a formula list for Prover9 (acommon theorem prover) and use it to perform a proof by refutation of thefollowing queries. You can download and install Prover9 and access on-linedocumentation at http://www.cs.unm.edu/∼mccune/prover9. To install it onomega, download the Linux code and compile it using the given instruc-tions. The install directory will also contain examples (additional ones canbe found on the web site). For each proof, include a printout of the output ofProver9.a) W oman(Mary) ∧ Son(Jack , Mary)b) Married(John, M ary) ∧ M arried(J ohn, Jane)c)∗∀x(Married(John, x) ⇒ Mother(x, Jack))d)∗Son(Jack, Jane) ∨ ¬M arried(J ohn, Jane)2013 Manfred Huber Page