Course - Logic and Proof MT24
- 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
- From the previous year:
- 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
- Related: [[Course - Logic MT24]]U
- Other courses this term: [[Courses MT24]]U
- Other resources:
Timetable
- Monday 9AM-10AM, weeks 1-8 (lecture)
- Tuesday 9AM-10AM, weeks 1-8 (lecture)
- Tuesday 3PM-4PM, weeks 3,5,7,8 (class)
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, Resolution]]U
- [[Notes - Logic and Proof MT24, Cutting planes]]U
- [[Notes - Logic and Proof MT24, Compactness theorem]]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, 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, Decidability results for first-order logic]]U
Problem Sheets
To-do List
- Go over notes on [[Notes - Logic and Proof MT24, Walk-SAT]]U and improve analysis my modelling as a “random walk on line $\{0, \ldots, n\}$ with absorbing barrier $0$ and reflecting barrier $n$”, and details for the 2-CNF case in which case the randomised algorithm only takes polynomial time
- Non constructive proof of the existence of interpolant in [[Notes - Logic and Proof MT24, Resolution]]U
- Constructive proof of the existence of interpolant in [[Notes - Logic and Proof MT24, Resolution]]U, also use extra notes made during lecture 3 and 4, “unzipping the original proof”
- Proof for lower bounds on resolution in [[Notes - Logic and Proof MT24, Resolution]]U
- Proof for lower bounds on resolution based on results about circuit lower bounds
- Example applications of compactness theorem
- Decidability of unbounded dense linear orders
-
Decidability of ordered divisible Abelian groups
- Make it more concrete using $\mathbb R$ with rational multiplication as an example
- Decidability of $\pmb T _ {RG}$
- Definition of a model
- Winning strategies in some [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]U
- Previous years notes would also be good to look at, e.g. the final 2023 lecture contains more material on [[Notes - Logic and Proof MT24, Ehrenfeucht-Fraïssé games]]U, especially the last proof that there is no first-order formula over the signature of graphs that represents the property of a graph being connected
- Better notes on using EF games to show completeness, etc.
- Slides give another proof for two graphs that can’t be distinguished where one is connected and the other is not, I think there is a typo in the notes where it says $2^{k}-1$ instead of $2^{k-1}$ (or maybe even $\ge 2^{k-1}+1$?)
- “Skolemization” spelling consistency?
- Proof of soundness in lecture 13
- High-level explanation of unification and resolution
- Proofs for completeness of first-order resolution
- Go over problem sheet solutions
- Lecturer said he likes ground resolution questions
- Compactness theorem for first order logic
- Vaught’s test, sufficient conditions for a theory to be complete (Theorem 10.6 in Logic)
- Proof of Ax-Grothendieck theorem using completeness of algebraically closed fields