Question 2 [SAT & Predicate Logic] (a) (i) Let po. p.90.91.ro,r1 be atoms capturing the states of three cells called p, q, and r, that can each either hold a 0 or a 1: Pi captures the fact that cell p holds the value i, and similarly for the other atoms. Consider the following formula: (po V p) (90 V91) ^ (roVm)^(-PO V-P.) (-90 V-9)^(-V-7) A(PO V go Vro) (P1 V91)^(P1V)^(91 V) Using DPLL, prove whether the above formula is satisfiable or not. Detail your answer. What property of the three cells p, q, and r, is this formula capturing? [4 marks] (ii) Given a CNF (Conjunctive Normal Form) that contains a clause composed of a single literal, can it be proved using Natural Deduction? Justify your answer. [2 marks] (b) Consider the following domain and signature: Domain: N Function symbols: zero (arity 0); succ (arity 1); * (arity 2) Predicate symbols: even (arity 1); odd (arity 1); = (arity 2) We will use infix notation for the binary symbols * and =. Consider the following formulas that capture properties of the above predicate symbols: let S, be Vx.(even(x) + 3y.x = 2 *y) let Sy be Vx.((ay.x = succ(2* y)) odd(x)) let Sz be Vx. Vy.(x = y + succ(x) = succ(y)) where for simplicity we write 0 for zero, 1 for succ(zero), 2 for succ(succ(zero)), etc. (0) Provide a constructive Sequent Calculus proof of: S1, S2, S3 +Vx.(even(x) odd(succ(x))) [6 marks) (ii) Provide a model M such that Fm Vx.(even(x) + odd(succ(x)) [2 marks] (ii) Provide a model M such that - Em Vx.(even(x) + odd(succ(x))) [2 marks] (c) Let p be a predicate symbol of arity 1 and q be a predicate symbol of arity 2. Let F be the Predicate Logic formula (Vx.(p(x)^3y.q(x,y))) +Vx.Jy (p(x) 19(x,y)). Provide a constructive Natural Deduction proof of F. You are not allowed to make use of further assumptions so all your hypotheses should be canceled in the final proof tree. [4 marks]