Lecture: Wednesday, 12-14, Room 139
Exercise: Wednesday, 14-16, Room 139
(The description in Zapisow is outdated)
The schedule below is from a previous year. There will be significant
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
Topics related to own research: Use of 3-valued logic for
modeling undefinedness. Theorem proving in 3-valued logic.
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.
02.03.2016. Resolution. Clauses, CNF-transformation.
09.03.2016. Examples of CNF-transformation. Ordering Refinements.
Given Clause Algorithm. Rules of Ground Superposition.
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).
13.04.2016. Propositional logic, DPLL, CDCL.
some more slides, written by
Leonardo de Moura.
If you want to read more about sat solving, you can visit
20.04.2016. More about SAT-solving. How to solve Sudoku's
27.04.2016. Circuit verification using
propositional logic. This is the
This is a specification of correctness of subtraction using
04/11.05.2016. No lecture!
18.05.2016. We did some small examples
We proved that reversing a list twice results in the same list.
We proved commutativity, and associativity of addition.
25.05.2016 is a
05.06.2013. Superposition in the non-ground case.