Logic and Proof supervisions

This course has three supervisions over the Lent term. I recommend you and your partner book all of your supervisions NOW — this will help to prevent supervisions bleeding into your well-earned holidays:) (If none of the available times on KuDoS work for you, please let me know.)

I prefer submitted work to be LaTeXed. If you’re finding it difficult to lay out proof trees, here’s a LaTeX package for proof-building to avoid the nested frac{}{} malarkey (link).

Supervision 1

  1. Parts (b) and (c) of 2017P6Q6 (link)
  2. Part (b) of 2015P6Q6 (link)
  3. Parts (a) and (b) of 2010P6Q6 (link)
  4. I am trying to prove safety properties of digital circuits with a theorem prover using propositional logic. What are the practical advantages and disadvantages of using first-order logic for this application instead? (Hint: what’s the domain?)

Supervision 2

  1. Part (a) of 2019P6Q9 (link)
  2. 2016P6Q5 (link)
  3. Assuming the three statements (a) \(H \rightarrow M \vee N\), (b) \(M \rightarrow K \wedge P\), and (c) \(N \rightarrow L \wedge P\), prove \(H \rightarrow P\) using clause resolution.
  4. 2020P6Q9 (link)
  5. (Optional) — From the notes, DPLL has five steps. For each, justify why it is necessary for the algorithm to work.

Supervision 3

  1. Part (b) of 2019P6Q10. For (i) and (ii) use tableau calculus, for (iii) use sequent calculus. (link)
  2. Part (b) of 2019P6Q9 (link)
  3. Part (d) of 2021P6Q10 (link)
  4. 2016P6Q6 (link)

If you’re having trouble understanding BDDs: link