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