Theorem Proving
Lecture: Wednesday, 1214, Room 139
Exercise: Wednesday, 1416, Room 139
Summary
(The description in Zapisow is outdated)

Theorem Proving in classical firstorder logic with equality.
Clauses, Transformation of firstorder 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 NPcomplete,
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 3valued logic for
modeling undefinedness. Theorem proving in 3valued 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, CNFtransformation.
Slides.

09.03.2016. Examples of CNFtransformation. 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 Eprover.
Use of TPTP.
Some (simple) example inputs:
Exercise list 1(3B),
Exercise list 2(5),
Exercise list 2(6).

06.04.2016.
Nonground 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 SATsolving. 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
twocomplement 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 nonground case.
Slides.
Exercises