Literature
Automated Reasoning
Script
| Date | Slides | Script | Notes | Other |
|---|---|---|---|---|
| Oct 26, 2022: | Slides | Script | Notes | |
| Oct 27, 2022: | Slides | Script | Notes | |
| Nov 02, 2022: | Slides | Script | Notes | |
| Nov 03, 2022: | Slides | Script | Notes | |
| Nov 09, 2022: | Slides | Script | ||
| Nov 10, 2022: | Slides | Script | ||
| Nov 16, 2022: | Slides | Script | Notes | |
| Nov 17, 2022: | Slides | Script | Notes | |
| Nov 23, 2022: | Slides | Script | Notes | |
| Nov 24, 2022: | Slides | Script | Notes | |
| Nov 30, 2022: | Slides | Script | Notes | |
| Dec 01, 2022: | Slides | Script | ||
| Dec 07, 2022: | Slides | Script | ||
| Dec 14, 2022: | Slides | Script | Notes | |
| Dec 15, 2022: | Slides | Script | Notes | |
| Dec 21, 2022: | Slides | Script | ||
| Dec 22, 2022: | Slides | Script | ||
| Jan 04, 2023: | Slides | Notes | ||
| Jan 05, 2023: | Slides | Script | Notes | |
| Jan 11, 2023: | Slides | Script | Notes | |
| Jan 12, 2023: | Slides | Script | Notes | SPASS Input PCP |
| Jan 18, 2023: | Slides | Script | Notes | Array Theory |
| Jan 19, 2023: | Slides | Script | Notes | |
| Jan 25, 2023: | Slides | Script | Notes | |
| Jan 26, 2023: | Slides | Script | Notes | |
| Feb 01, 2023: | Slides | Script | Notes | |
| Feb 08, 2023: | Slides | Notes |
Course material from other lectures
- Harald Ganzinger, Viorica Sofronie-Stokkermans, Uwe Waldmann:
Slides for "Automated Reasoning" SS 2004.
Online at http://people.mpi-inf.mpg.de/~uwe/lehre/autreas/readings.html. - Gert Smolka:
Lecture notes for "Einführung in die Computationale Logik" SS 2003.
Online at https://www.ps.uni-saarland.de/courses/cl-ss03/skript/.
Propositional logic, first-order logic, tableaux calculi
- Melvin Fitting:
First-Order Logic and Automated Theorem Proving.
Springer-Verlag, New York, 1996. - Uwe Schöning:
Logik für Informatiker.
Spektrum Akademischer Verlag, 2000. - Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (Editors):
Handbook of Satisfiability - Second Edition.
IOS Press, 2021. - Uwe Schöning, Jacobo Torán:
The Satisfiability Problem - Algorithms and Analyses.
Lehmanns Verlag, 2013.
Termination, well-founded orderings, confluence, unification
- Franz Baader and Tobias Nipkow:
Term Rewriting and All That.
Cambridge Univ. Press, 1998
Further readings
- Leo Bachmair and Harald Ganzinger
Resolution Theorem Proving, in "Handbook of Automated Reasoning", pages 19-99.
Elsevier, 2001. - Robert Nieuwenhuis and Albert Rubio
Paramodulation-Based Theorem Proving, in "Handbook of Automated Reasoning", pages 371-443.
Elsevier, 2001. - Andreas Nonnengart and Christoph Weidenbach
Computing small clause normal forms, in "Handbook of Automated Reasoning", pages 335-367.
Elsevier, 2001. - Christoph Weidenbach
Combining Superposition, Sorts and Splitting, in "Handbook of Automated Reasoning", pages 1965-2012.
Elsevier, 2001.