(a) (i) Let Po, P1, 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: p; captures the fact that cell p holds the value i, and similarly for the other atoms. Consider the following formula: (po V p.) ^ (90 V q) ^ (rovri)(-po V-p1)^(-90 V-91)^(-ro Var) ^(po V90 V ro) ^ (P1 V 91) ^ (P1 V r) ^ (91 V r) 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? (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. (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 Si be Vx.(even(x) + 3y.x = 2*y) let S2 be Vx.((Ey.x = succ(2 * y)) odd(x)) let S3 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. (i) Provide a constructive Sequent Calculus proof of: S1, S2, S3 +Vx.(even(x) odd(succ(x))) (ii) Provide a model M such that EM Vx.(even(x) + odd(succ(x))) (iii) Provide a model M such that EM Vx.(even(x) + odd(succ(x))) (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 (Wx.(p(x) 1 3y.q(x, y))) Vx.3y.(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. (a) (i) Let Po, P1, 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: p; captures the fact that cell p holds the value i, and similarly for the other atoms. Consider the following formula: (po V p.) ^ (90 V q) ^ (rovri)(-po V-p1)^(-90 V-91)^(-ro Var) ^(po V90 V ro) ^ (P1 V 91) ^ (P1 V r) ^ (91 V r) 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? (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. (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 Si be Vx.(even(x) + 3y.x = 2*y) let S2 be Vx.((Ey.x = succ(2 * y)) odd(x)) let S3 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. (i) Provide a constructive Sequent Calculus proof of: S1, S2, S3 +Vx.(even(x) odd(succ(x))) (ii) Provide a model M such that EM Vx.(even(x) + odd(succ(x))) (iii) Provide a model M such that EM Vx.(even(x) + odd(succ(x))) (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 (Wx.(p(x) 1 3y.q(x, y))) Vx.3y.(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