# 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.

## (Outdated) Schedule

• 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.