COM2107
Data Provided: None
DEPARTMENT OF COMPUTER SCIENCE Spring Semester 2019-20
Logic in Computer Science 2 hours
Answer FOUR questions.
All questions carry equal weight. Figures in square brackets indicate mark per-
centages available per question part.
COM2107 1 TURN OVER
COM2107
This page is blank.
COM2107 2 CONTINUED
COM2107
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 {¬p ∧ ¬q, p ∨ q} is inconsistent. [20%]
d) (i) Define 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) ∃x. (P (x) ∨Q(x)) ` ∃x. P (x) ∨ ∃x. Q(x). [20%]
(ii) ¬∀x. P (x) ` ∃x. ¬P (x). [20%]
b) Which of the following expressions are formulas of predicate logic? Explain why.
(i) ∀X∀Y. (X ⊆ Y ↔ (∀x. x ∈ X → x ∈ Y )). [10%]
(ii) ∀P. P (0) ∧ ∀n. (P (n)→ P (n+ 1))→ (∀n. P (n)). [10%]
(iii) ∀t. G(P (t)U P (t)), where P is a predicate symbol. [10%]
c) Consider the signature ΣA = {+, ·, 0, 1} 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 7→ 11N step-by-step. [20%]
d) Show that the formula ∀x∀y. (f(x, y) = f(y, x)) is satisfiable, but not valid. [10%]
COM2107 3 TURN OVER
COM2107
3. a) Consider the clause sets
S0 = {{p,¬q}, {q, r}, {¬p,¬q, r}, {¬r}},
S1 = {{p, q}, {¬p,¬q}, {q, r}, {¬q,¬r}, {r, p}, {¬r,¬p}}.
(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 unifiers for the following sets, if they exist.
(i) {x ≈ f(a), g(x, x) ≈ g(x, y)}. [10%]
(ii) {f(g(a, x), g(b, x)) ≈ f(g(b, x), z)}. [10%]
e) Use resolution to prove that ∃x. (P (x)→ ∀y. 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 traffic light will eventually become green when
someone pushes the button. [10%]
(ii) The light blinks finitely many times. [10%]
(iii) Lions and zebras never drink together at the water hole. [10%]
END OF QUESTIONS
COM2107 4
COM2107
Data Provided: None
DEPARTMENT OF COMPUTER SCIENCE Spring Semester 2018-19
Logic in Computer Science 2 hours
Answer FOUR questions.
All questions carry equal weight. Figures in square brackets indicate the per-
centage of available marks allocated to each part of a question.
COM2107 1 TURN OVER
COM2107
This page is blank.
COM2107 2 CONTINUED
COM2107
1. a) Professor Wright says that students will fail the exam if they don’t get implication.
Dana fails, but gets implication. Is Professor Wright wrong? [10%]
b) Define negation in terms of other propositional connectives. [10%]
c) The equation Jϕ⊕ψKv = (JϕKv + JψKv)− 2 · JϕKv · JψKv defines the semantics of the
exclusive or operation ⊕. Write down natural deduction rules for it. [15%]
d) Prove the following sequents using natural deduction.
(i) ¬(p ∧ q) ` ¬p ∨ ¬q. [20%]
(ii) ` p ∨ (p ∧ q)→ p. [20%]
e) Why is the satisfiability problem of propositional logic decidable? [10%]
f) (i) For which assignments v is J(p ∧ ¬q)→ rKv = 0? [5%]
(ii) Compute J(p ∧ ¬q)→ rKv step by step for these. [10%]
COM2107 3 TURN OVER
COM2107
2. a) Translate the following sentences into predicate logic.
(i) Every natural number has precisely one successor. [10%]
(ii) No pair of adjacent vertices (in some graph) has the same colour. [10%]
b) Prove ¬∀x. P (x) ` ∃x. ¬P (x) by natural deduction. [20%]
c) The signature of monoids consists of a binary function symbol · and a constant symbol
1. The following associativity and identity axioms hold in every monoid.
∀x, y, z. (x · y) · z = x · (y · z), ∀x. 1 · x = x, ∀x. x · 1 = x.
Prove with natural deduction that the identity 1 is uniquely defined. [20%]
d) Write down the definitions for the assignment function v for predicate logic and the
interpretation function J−KAv of Σ-terms in a Σ-structure A. [10%]
e) Consider the signature ΣA = {+, ·, 0, 1} 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 7→ 11N for variable x. [20%]
f) What does A |=v ϕ mean? [10%]
COM2107 4 CONTINUED
COM2107
3. a) The Shannon expansion of a propositional formula ϕ is the formula
(¬p ∧ ϕ[⊥/p]) ∨ (p ∧ ϕ[>/p]).
Use the property ϕ↔ (¬p∧ϕ[⊥/p])∨(p∧ϕ[>/p]) to compute the Shannon expansions
of the following propositional formulas, expanding first with respect to p and then with
respect to q. Simplify the results as much as possible by propositional reasoning.
(i) p⊕ q. [20%]
(ii) p→ (q → p). [20%]
b) Construct a binary decision tree for p ∧ (p ∨ ¬r). Label its root with p, its children
with q and its grandchildren with r. [10%]
c) Show that Skolemisation doesn’t preserve validity. [10%]
d) Prove that {{¬p, r}, {¬q, r}, {p, q}, {p,¬r}, {q,¬r}, {¬r}} is inconsistent
(i) using the DPLL method; [20%]
(ii) using resolution. [20%]
COM2107 5 TURN OVER
COM2107
4. a) (i) Draw a graph for the LTS (S,→, λ) with [15%]
S = {s0, s1, s2, s3},
→ = {(s0, s0), (s0, s1), (s2, s1), (s1, s2), (s2, s2)},
λ : s0 7→ {p, q}, s1 7→ {r}, s2 7→ {p, r}, s3 7→ {t}.
(ii) Compare with the definition from the lectures. What is wrong? [5%]
b) Define the LTL operators F and G in terms of U . Justify your choices. [20%]
c) Prove or refute F (ϕ ∧ ψ) ≡ Fϕ ∧ Fψ. [10%]
d) Check the following properties of LTL formulas on the LTS S defined by
s0
r
s1
p, q
s2
p, t, r
s3
q, r
(i) S, s0 |= ¬p→ r, [10%]
(ii) S, s0 |= Fq, [10%]
(iii) S, s3 |= Ft, [10%]
(iv) S, s0 |= G(r ∨ q). [10%]
(v) S, s0 |= (p ∨ r)U(q ∨ t). [10%]
END OF QUESTIONS
COM2107 6










































































































































学霸联盟