FORMAL LOGIC

Computer Science School of Computing

4.1 Convert the formula (xp(x)yq(y,y))x(p(x)yq(x,y)) to clausal form. Use the commutativity of and to minimise the number of skolem functions. Show all the steps. 4.2 Give the (i) Herbrand universe, (ii) the Herbrand base, and (iii) a Herbrand model, for the following set of first-order clauses. {{p(f(x),x)},{p(g(x),y)}} 4.3 Prove by resolution refutation that the following set of clauses is unsatisfiable. {{p(f(y)),q(x,y)},{q(x,a),r(f(x))},{p(x),r(x)},{q(f(x),a),r(x)},{q(f(f(z)),z)}} For each step, indicate the substitutions used and the numbers of parent clauses. (8) 4.4 Consider the following logic program: 1. p(a,x,x) 2. p(f(x),y,f(z))p(x,y,z) 3. p(x,f(y),f(z))p(x,y,z) Draw an SLD-tree to show all attempts to answer each of the following queries: (i) p(f(a),f(a),f(f(a))) (ii) p(f(a),f(x),f(a)) Use the selection rule that resolves on the leftmost literal