Syllabus
- basic concepts, syntax, semantics
- propositional Resolution system, feasible interpolation, SAT solvers,\dots
- 3 main formalizations of proofs: Hilbert/Frege style, Gentzen's sequent calculus, Natural Deduction
- the Cut-elimination Theorem and its applications
- Herbrand's Theorem
- bounds on the size of cut-free proofs and Herbrand's disjunction
- first-order Resolution and automated theorem proving
- selfreference, Godel's theorems, Rosser's theorem
- if time permits more
Annotation
In this course students will get acquainted with basic concepts of proof theory (proof systems for propositional and predicate logics) and basic results of this theory (Herbrand's theorem, cut-elimination theorem, Craig's interpolation theorem). These results will be studied from the point of view of complexity; we shall present also some lower bounds.
Further the course will cover some results on term rewriting and we shall also recall Godel's incompleteness theorems.