Clausal Form [15 points]Unification II [20 points]Unification II [10 points]Unification III [15 points]Factors [10 points]Resolution I [10 points]Resolution II [20 points]CS157: Computational Logic (2010-11)Assignment 3, Due Thursday November 4 at 11:59 pmOctober 28, 2010Please see the course website for homework submission policy. collaboration policy andregrade policy.You may use Logica with acknowledgement. You may work in groups of upto three. Acknowledge all aid and collaboration. Please abide by the Honor Code.Submission Instructions: Mail your assignment to [email protected] hard copies will be accepted.File Name Instructions: Please name your files as [first name]-[lastname]-[assignment#].[file format]. If you are John Doe submitting Assginment 3, you should name yourfile John-Doe-3 .1 Clausal Form [15 points]Convert the following sentence to clausal form. You MUST show your all of your work toreceive full credit.∃w.∀x.(∃y.(¬p(x, y) ∧ r(y)) ⇐ ∃z.(q(w, z)))2 Unification II [20 points]Determine whether each of the following pairs of expressions is unifiable. If yes, give amost general unifier. No explanation is necessary.(a) p(x, b, f(y)) and p(a, y, f(z))(b) p(f(x, b), g(y), f (z, a)) and p(y, g(f(g(w), w)), f(w, z))(c) p(f(g(a)), x, f (h(z, z)), h(y, g(w))) and p(y, g(z), f(v), h(f(w), x))13 Unification II [10 points](a) Assuming that x, y, z, v, and w are variables, give a most general unifier for the expres-sions p(t(x, y), r(z, z)) and p(t(t(w, z), v), w).(b) Is it possible for two expressions to have more than one most general unifier? If so,give a simple example. If not, give a brief explanation.4 Unification III [15 points]Suppose that γ and δ are unifiers for expressions in relational logic. Which of the followingare true? Briefly explain your answer to get full credit. In these questions, γδ denotes thevariable substitution resulting from the composition of γ and δ. As usual, you may assumethat all unifiers are pure, i.e. the variables being replaced do not occur within any of thereplacements.(a) If γ is a most general unifier, then there is a substitution θ such that γθ=δ.(b) If γ is a unifier, but not a most general unifier, then there is a variable substitution θsuch that γθ is a most general unifier.(c) If γ and δ are most general unifiers, then γδ is a most general unifier.5 Factors [10 points]Determine whether the following clauses have nontrivial factors (factors besides the clauseitself). If yes, say ‘Yes’ and give all the nontrivial factors. If no, simply state ‘No’. Noexplanation is necessary.(a) {p(x, y), q(a, b), ¬p(b, a), q(y, x)}(b) {p(x, y), q(a, b), ¬p(b, a), ¬q(y, x)}(c) {p(x, f(y)), p(g(u), x), p(f (y), u)}(d) {p(g(x)), q(x), p(f(a)), p(x), p(g(f (x))), q(f (a))}6 Resolution I [10 points]Find all single-step resolvents (if any) of the following pairs of clauses. If there are none,simply state ‘none’.(a) {¬p(x), q(x, x)} and {¬q(a, f (a))}(b) {¬p(x, y, u), p(u, y, w)} and {p(g(x, y), x, y)}27 Resolution II [20 points]Give a resolution proof that these premises:1. ∃x.∀y.(p(x, y) ⇔ q(x, y))2. ∀x.(∃y.p(x, y) ∨ ∃z.q(x, z))entail this conclusion:∃x.∃y.(p(x, y) ∧ q(x, y))(Optional) FeedbackTell us what you thought about this problem set:1. How hard was it overall? Give a number from 1-10, with 1 being way too easy and10 being way too hard and 5 being just right.2. Comment on individual problems. Were any particularly interesting? Any partic-ularly difficult? Which, if any, helped you understand the material better? Whichshould be eliminated and why?3. Any other
View Full Document
Unlocking...