Course - Logic and Proof MT24

This course covers topics in logic and proof from a computer science perspective. The start of the course covers some problems in propositional logic, such as compactness, proving that the $\mathsf{SAT}$ problem for some classes of formulas can be solved in polynomial time, and that simple resolution proofs can lead to exponentially long refutations. Then the course moves onto topics in first-order logic, such as Ehrenfeucht-Fraïssé games and looking at decidable theories. Then it finally covers the compactness of first-order logic and shows that the satisfiability and validity problem for first-order logic is actually undecidable.

• Course webpage
• Lecture notes
  • 0, Propositional logic preliminaries: notes
  • 1, Polynomial time formula classes: notes, slides
  • 2, Resolution and interpolation: notes, slides
  • 3, Lower bounds for resolution: notes, slides
  • 4, Cutting planes: notes, slides
  • 5, Compactness theorem: notes
  • 6, Primer on first-order logic: notes
  • 7, Decidable theories, part one: notes
  • 8, Decidable theories, part two: notes, slides
  • 9, Algebraically closed fields: notes, slides
  • 10, Ehrenfeucht-Fraïssé games: notes, slides
  • 11, Herbrand’s theorem: notes, slides
  • 12, Undecidability of validity and satisfiability: notes, slides
  • 13, Unification and resolution: notes, slides
  • 14, Compactness and lower bounds: notes
• My notes here are based on the lecture notes above, written by Prof. James Worrell.
• Related: [[Course - Logic MT24]]^U
• Other courses this term: [[Courses MT24]]^U

Notes

• [[Notes - Logic and Proof MT24, All the algorithms]]^U
• [[Notes - Logic and Proof MT24, Basic definitions for propositional logic]]^U
• [[Notes - Logic and Proof MT24, Horn formulas]]^U
• [[Notes - Logic and Proof MT24, 2-CNF formulas]]^U
• [[Notes - Logic and Proof MT24, Walk-SAT]]^U
• [[Notes - Logic and Proof MT24, 3-CNF formulas]]^U
• [[Notes - Logic and Proof MT24, XOR-Clauses]]^U
• [[Notes - Logic and Proof MT24, Boolean circuits]]^U
• [[Notes - Logic and Proof MT24, Propositional resolution]]^U
• [[Notes - Logic and Proof MT24, Interpolants]]^U
• [[Notes - Logic and Proof MT24, Lower bounds for resolution]]^U
• [[Notes - Logic and Proof MT24, Cutting planes]]^U
• [[Notes - Logic and Proof MT24, Compactness theorems]]^U
• [[Notes - Logic and Proof MT24, First-order logic]]^U
• [[Notes - Logic and Proof MT24, Logical theories]]^U
• [[Notes - Logic and Proof MT24, Decidable theories]]^U
• [[Notes - Logic and Proof MT24, Quantifier elimination]]^U
• [[Notes - Logic and Proof MT24, Unbounded dense linear orders]]^U
• [[Notes - Logic and Proof MT24, Rado graph]]^U
• [[Notes - Logic and Proof MT24, Regular languages]]^U
• [[Notes - Logic and Proof MT24, Presburger arithmetic]]^U
• [[Notes - Logic and Proof MT24, Algebraically closed fields]]^U
• [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]^U
• [[Notes - Logic and Proof MT24, Skolemization]]^U
• [[Notes - Logic and Proof MT24, Herbrand’s theorem]]^U
• [[Notes - Logic and Proof MT24, Ground resolution]]^U
• [[Notes - Logic and Proof MT24, Unification and resolution]]^U
• [[Notes - Logic and Proof MT24, Vaught’s test]]^U
• [[Notes - Logic and Proof MT24, Decidability results for first-order logic]]^U
• [[Notes - Logic and Proof MT24, Lower bounds for deciding real arithmetic]]^U

Problem Sheets

• Sheet 1, partial solutions
• Sheet 2
• Sheet 3
• Sheet 4

To-do List

Previous course materials

The course was a bit different in previous years since there was no introductory [[Prelims]]^U logic course.

• Notes
  • 1, Introduction: notes, slides
  • 2, Propositional logic: notes, slides
  • 3, Equivalence and normal forms: notes, slides
  • 4, Polynomial time formula classes: notes, slides
  • 5, Resolution: notes, slides
  • 6, DPLL algorithm: notes, slides
  • 7, Lower bounds for resolution: notes
  • 8, Compactness theorem: notes, slides
  • 9, First-order logic: notes, slides
  • 10, Normal forms for first-order logic: notes, slides
  • 11, Herbrand’s theorem and ground resolution: notes, slides
  • 12, Examples of ground resolution proofs: notes
  • 13, Undecidability of validity and satisfiability: notes, slides
  • 14, Resolution for predicate logic: notes, slides
  • 15, Decidable theories: notes
  • 16, Compactness theorem and Vaught’s test: notes, slides
• Problem sheets
  • Sheet 1
  • Sheet 2
  • Sheet 3
  • Sheet 4
  • Sheet 5