COM2107 Logic in Computer Science

Spring term 2023/24

Exercise Sheet 11

Generic question types:

• questions about terminology and bookwork questions,

• questions about computations and deductions (how to apply methods and rules),

• questions about the comprehension of methods and rules (understanding semantics and consequences of theorems such as completeness, compactness, decidability)

• questions about transferable knowledge and skills (applications of knowledge about logic to new tasks beyond lectures)

Examples about computations and deductions:

Question 11.1 Indicate which of the following unification problems have a solution.

(a)  x ≈ f (a), g(x, x) ≈ g(x, y).

(b)  f (g(a, x), g(y, b)) ≈ f (g(b, x), z).

(c)  f (g(a, x), g(y, b)) ≈ f (g(a, y), x).

(d)  k(f (x, g(a, y)), g(x, h(y))) ≈ k(f (h(y), g(y, a)), g(z, z)).

Question 11.2 Indicate which of the following pairs of LTL formulas are equivalent.

1.  FF ϕ and F ϕ .

2.  ϕU (ϕUψ) and ϕUψ .

3.  (ϕUψ)Uψ and ϕUψ .

4.  (ϕ ∨ ψ)Uχ and (ϕUχ) ∨ (ψUχ).

5.  Gϕ and ϕ ∧ XGϕ .

Question 11.3 Which result does the DPLL algorithm compute on the following input set?

{{p, q}, {¬p, q}, {p, ¬q}, {¬p, ¬q}}

• Option 1

• Option 2

• Option 3

• Option 4

Question 11.4 Which is the Skolem normal form of the following formula?

¬ ((∀x. (P ∨ Q(x))) → P ∨ ∀x. Q(x))

• Option 1

• Option 2

• Option 3

Question 11.5 Does resolution refute the following formula?

(∃y∀x. P (x, y)) → (∀x∃y. P (x, y))

• Yes.

• No.

Question 11.6 The labelled transition system M is defined by

Indicate which of the following properties of LTL formulas are true:

(a)  M, s0  |= ¬p → r ,

(b)  M, s0  |= Ft and M, s3  |= Ft,

(c)  M, s0  |= Fq ,

(d)  M, s0  |= G(r ∨ q).