PMT Problems

I was an Undergraduate Teaching Assistant for the 14/15 and 15/16 academic years at Imperial College London. I’ve uploaded some of the materials I’ve used as these were generally quite well-received by the students, and could be useful to other PMT groups and/or people interested in these subjects.

I should add a note of caution that the groups I tutored were relatively strong, and I designed these problem sheets to be challenging for strong students. The last parts/last few problems on each sheet tend to be considerably more difficult than the material covered in the lecturers’ tutorial sheets and (most of) the exams.

140 Logic
Note that the numbers on the files are offset relative to the sequence numbers presented here, because they correspond to the week of the term in which I went through the relevant exercise with the students.

  1. Recurrence Relations and Boolean Satisfiability: I introduced the students to dynamic programming, as well as to various variants of the well-known SAT problem.
  2. Propositional Logic Translations: This sheet covers translating English statements to propositional logic. Be mindful of some… traps.
  3. 2SAT: We look at a variant of the NP-complete SAT problem, 2SAT, and analyse an algorithm to solve it, concluding that it is actually in P. Some of the ideas for this tutorial sheet were taken from the 438 Complexity course at Imperial.
  4. Natural Deduction: We look at examples of natural deduction proofs using the Jaskowski (linear) style. This is typically a significant task in the exams the first year Logic students take.
  5. Attack of the Zombies (Predicate Logic Translations): Another battery of English to logic translations, though these are to first-order logic. Some of these get rather long; my usual advice involves divide and conquer.
  6. Static Program Verification and Random Haskell Functions: This coincides with the discussion of formal specifications for functions in the course. Some of the first part of the material was drawn from 440 Software Reliability.
  7. Christmas Test Revision: Computing students are required to take an examination in December which covers Logic, Mathematical Methods and Discrete Mathematics. This version of the sheet only covers Logic, because I taught a JMC group (and the students thus do not take either of the latter two subjects).

141 Reasoning about Programs

  1. Binet’s Formula and Graph Connection: A relatively light introduction to the term; we recap the notions of induction and strong induction, and look at a flawed proof.
  2. Divisibility: We prove the correctness of a few nontrivial tests for checking whether a number is divisible by another number.
  3. Colours and Longest Common Subsequence: We look at examples of structural induction over lists or pairs of lists in Haskell.
  4. Binary Strings and Max Subarray Sums: We again explore further examples of structural induction, including a messier example involving higher-order functions.
  5. Computation Tree Logic (missing pdf – I’ll look for it): We introduce the temporal logic CTL as well as explicit-state model checking algorithms for CTL. We prove the correctness of fixpoint algorithms for determining the sets of states in which the connectives AX, AF and EU hold. The idea for this tutorial originated from 303 Systems Verification. (This sheet is difficult.)
  6. Ternary Chop and Golden Section Search: We consider loop invariants and their role in proving the correctness of nontrivial functions. Problem 2 involves a relatively tricky challenge of determining an inductive invariant as well. I drew inspiration from another course at Imperial – 477 Computing for Optimal Decisions. (This sheet was harder than expected.)
  7. Formalism and Transitive Closures: I received some solutions from students that were correct in substance but not always properly expressed in terms of style; the first problem involved marking a proof with many planted flaws. The second problem looked at the correctness of Warshall’s algorithm and its extension to solving All Pairs Shortest Paths.
  8. Memory Lane, Peaks and Fallout: This was the final session. We covered several relatively simple problems from Logic, a fairly straightforward loop induction proof, and a somewhat more complex construction involving dynamic programming with nested loops. (Problem 3 is somewhat difficult.)

142 Discrete Mathematics

  1. Project Purity: This wasn’t actually given to my tutorial group (as it was written only in year 4 and I took a JMC group), but is an example of what I would probably have given as the “final challenge” to a strong group of students. This involves proving correctness of the push-relabel algorithm for computing maximum flows in a graph. I filed this under DM as opposed to Reasoning as the quantisation of detail is substantially lower, owing to the significant complexity of the task. (I’d say for a first-year student this is very difficult.)

Additional Problems
I have a few extra questions that didn’t make the final tutorial sheets (usually owing to limited time, excess difficulty etc.) which I’ll leave here.

(Coming soon)