Theorem Proving

Lecture: Wednesday, 12-14, Room 139
Exercise: Wednesday, 14-16, Room 139

Summary

(The description in Zapisow is outdated)

Theorem Proving in classical first-order logic with equality. Clauses, Transformation of first-order logic to clausal normal form. Unification, Resolution, Superposition. Other Methods for Automated Proof Search (TABLEAUX).
Theorem proving in classical propositional logic. DPLL Algorithm. Solving propositional logic is NP-complete, but modern techniques for theorem proving are so good, that they are used used for circuit verification. We also study applications to theory reasoning.
Interactive Theorem Proving using Isabelle.
Topics related to own research: Use of 3-valued logic for modeling undefinedness. Theorem proving in 3-valued logic.

The schedule below is from a previous year. There will be significant changes.

24.02.2016. First lecture. We say hello to each other, and find out each other's background knowledge. It turns out, that I was able to treat some material. introduction, and sequent calculus.
02.03.2016. Resolution. Clauses, CNF-transformation. Slides.
09.03.2016. Examples of CNF-transformation. Ordering Refinements. Given Clause Algorithm. Rules of Ground Superposition. Slides.
16.03.2016. ground superposition. Completeness Proof.
23.03.2016. Completeness proof of ground superposition. Demonstration of E-prover. Use of TPTP. Some (simple) example inputs: Exercise list 1(3B), Exercise list 2(5), Exercise list 2(6).
06.04.2016. Non-ground superposition. Slides.
13.04.2016. Propositional logic, DPLL, CDCL. slides. some more slides, written by Leonardo de Moura. If you want to read more about sat solving, you can visit SATLive.
20.04.2016. More about SAT-solving. How to solve Sudoku's using SAT.
27.04.2016. Circuit verification using propositional logic. This is the fast adder. This is a specification of correctness of subtraction using two-complement method.
04/11.05.2016. No lecture!
18.05.2016. We did some small examples in Isabelle. We proved that reversing a list twice results in the same list. We proved commutativity, and associativity of addition. ToyList.
25.05.2016 is a Thursday!
05.06.2013. Superposition in the non-ground case. Slides.