CS代写 | COM2107 Logic in Computer Science

本次英国代写主要为计算机与逻辑相关的quiz

COM2107 Logic in Computer Science

1. a) What is an assignment? [10%]
b) Prove the following sequents using intuitionistic natural deduction.
(i) p _ (q ^ r) ` (p _ q) ^ (p _ r). [20%]
(ii) ` ::(p _ :p). [20%]
c) Prove that the set of formulas f:p ^ :q; p _ qg is inconsistent. [20%]
d) (i) De ne a function that counts number of propositional connectives in a propo-
sitional formula (i.e., the number of internal nodes of its abstract syntax tree).
[10%]
(ii) Prove that if a propositional formula does not contain any negation symbol,
then it has more propositional variables (leaves of the abstract syntax tree)
than propositional connectives (internal nodes). [20%]
2. a) Prove the following formulas by natural deduction.
(i) 9x: (P(x) _ Q(x)) ` 9x: P(x) _ 9x: Q(x). [20%]
(ii) :8x: P(x) ` 9x: :P(x). [20%]
b) Which of the following expressions are formulas of predicate logic? Explain why.
(i) 8X8Y: (X  Y $ (8x: x 2 X ! x 2 Y )). [10%]
(ii) 8P: P(0) ^ 8n: (P(n) ! P(n + 1)) ! (8n: P(n)). [10%]
(iii) 8t: G(P(t) U P(t)), where P is a predicate symbol. [10%]

c) Consider the signature A = f+;
; 0; 1g of arithmetic, extended with constant symbols
for each natural number, and the A-structure N = (N;+N;

N; 0N; 1N). Interpret the
A-term 3
x + 9 in N with assignment v : x ! 11N step-by-step. [20%]
d) Show that the formula 8x8y: (f(x; y) = f(y; x)) is satis able, but not valid. [10%]

3. a) Consider the clause sets
S0 = ffp; :qg; fq; rg; f:p; :q; rg; f:rgg;
S1 = ffp; qg; f:p; :qg; fq; rg; f:q; :rg; fr; pg; f:r; :pgg:
(i) Use the DPLL algorithm to show that both are inconsistent. [20%]
(ii) Use resolution to show that both are inconsistent. [20%]
b) Resolution is refutationally complete for propositional logic. What does this mean? [10%]
c) Skolemisation of predicate logic formulas does not preserve validity. Why? [10%]
d) Compute the most general uni ers for the following sets, if they exist.
(i) fx  f(a); g(x; x)  g(x; y)g. [10%]
(ii) ff(g(a; x); g(b; x))  f(g(b; x); z)g. [10%]
e) Use resolution to prove that 9x: (P(x) ! 8y: P(y)) is valid. [20%]
4. a) Explain the model checking problem. [10%]
b) Prove or refute the following formulas.
(i) G’  ‘ ^ XG’. [20%]
(ii) F(‘ ^ )  F’ ^ F . [20%]
(iii) ‘U  _ (‘ ^ X(‘U )). [20%]
c) Translate the following statements into linear temporal logic.
(i) It is always the case that the trac light will eventually become green when
someone pushes the button. [10%]
(ii) The light blinks nitely many times. [10%]

(iii) Lions and zebras never drink together at the water hole. [10%]