Website Contents
Note: In case of questions or problems concerning this lecture, please contact Dr. Bubeck, either in person during his office hours or by email.
News
+++ Due to low enrollment, the lecture will not be given this semester. +++
General Information
| Lecturer: |
Dr. Uwe Bubeck |
| Exercises: | Dr. Uwe Bubeck |
| Type: | 2 hrs. lecture, 1 hr. exercises |
| Lecture: | Do 14-16 in D1.303 |
| Exercises: | Do 13-14 in E2.304 |
| Exam: | Oral; Master Module III.1.4 (SWT & IS) |
Automated or computer-assisted theorem proving has various advantages over manual proving with pen and paper. In particular, the computer can reveal fl aws and omissions in proofs, and there exist interesting applications in the area of software and hardware veri fication. Over the last decades, a wide range of different calculi for automated theorem proving have been developed. In this lecture, we will cover, e.g.:
- Resolution in fi rst-order logic and variants
- Equality handling, paramodulation
- Model elimination
- Tableaux
- Decision procedures and SAT solvers
- Implementation of resolution provers and SAT solvers
- Applications
Lecture Notes
Exercises
Further Reading
- Biere: Handbook of Satisfiability, IOS Press, 2009
- Fitting: First-Order Logic and Automated Theorem Proving, Springer, 1996
- Gallier: Logic for Computer Science, Wiley, 1986 / 2003
- Robinson: Handbook of Automated Reasoning Vol. 1&2, Elsevier, 2001