Nov 05 2020: Slides   Script   Bamboo

Nov 11 2020: Slides   Script   Bamboo

Nov 12 2020: Slides   Script   Bamboo   Fig2.9  Errata

Nov 18 2020: Slides   Script   Bamboo

Nov 19 2020: Slides   Script   Bamboo

Nov 25 2020: Slides   Script   Bamboo

Nov 26 2020: Slides   Script   Bamboo

Dec 02 2020: Slides   Script   Bamboo

Dec 03 2020: Slides   Script   Bamboo

Dec 09 2020: Slides   Script   Bamboo

Dec 10 2020: Slides   Script   Bamboo

Dec 16 2020: Slides   Script   Bamboo   Errata

Dec 17 2020: Slides   Script   Bamboo

Jan  06 2021: Slides   Script   Bamboo

Jan  07 2021: Slides   Script   Bamboo

Jan  13 2021: Slides   Script   Bamboo

Jan  14 2021: Slides   Script   Bamboo

Jan  20 2021: Slides   Script   Bamboo

Jan  21 2021: Slides   Script   Bamboo

Jan  27 2021: Slides   Script   Bamboo

Jan  28 2021: Slides   Script   Bamboo

Feb 03 2021: Slides   Script   Bamboo

Feb 04 2021: Final-Exer-Sol-1   Final-Exer-Sol-2

• English-German dictionary of deduction-related terms: [pdf]  [ps]

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

• 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
  IOS Press, 2009
• Uwe Schöning, Jacobo Torán:
  The Satisfiability Problem - Algorithms and Analyses
  Lehmanns Verlag, 2013

• Franz Baader and Tobias Nipkow:
  Term Rewriting and All That.
  Cambridge Univ. Press, 1998

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