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) Dene 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).
(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 satisable, 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 uniers 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%]
本网站支持 Alipay WeChatPay PayPal等支付方式
E-mail: email@example.com 微信号:vipnxx