Course - Logic and Proof MT24

Created: October 11, 2024
Updated: January 10, 2025

---

• 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
• Prof. James Worrell wrote the lecture notes for this course, and the notes here are adapted from those notes.
• Related: [[Course - Logic MT24]]^U
• Other courses this term: [[Courses MT24]]^U

Notes

• [[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, solutions
  • Sheet 3
  • Sheet 4
  • Sheet 5

---

Related posts

• [[Notes - Logic and Proof MT24, Interpolants]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, XOR-Clauses]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Decidability results for first-order logic]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Walk-SAT]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, 3-CNF formulas]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Ground resolution]]^U

  (incoming)
• [[Course - Logic MT24]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Horn formulas]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Herbrand's theorem]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Presburger arithmetic]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Cutting planes]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, First-order logic]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Skolemization]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Basic definitions for propositional logic]]^U

  (incoming)
• [[University Notes]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, 2-CNF formulas]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Lower bounds for resolution]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Decidable theories]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Lower bounds for deciding real arithmetic]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Boolean circuits]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Algebraically closed fields]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Vaught's test]]^U

  (incoming)
• [[Courses MT24]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Propositional resolution]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Unbounded dense linear orders]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Logical theories]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Regular languages]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Unification and resolution]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Quantifier elimination]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Compactness theorems]]^U

  (incoming)
• [[Notes - Logic and Proof MT24, Rado graph]]^U

  (incoming)
• [[Lecture - Models of Computation MT23, XII]]^U

  (sim: 0.605)
• [[Lecture - Models of Computation MT23, XIII]]^U

  (sim: 0.605)
• [[Lecture - Models of Computation MT23, XIV]]^U

  (sim: 0.605)