Automated Reasoning


Oct 26, 2022:SlidesScriptNotes 
Oct 27, 2022:SlidesScriptNotes 
Nov 02, 2022:SlidesScriptNotes 
Nov 03, 2022:SlidesScriptNotes 
Nov 09, 2022:SlidesScript  
Nov 10, 2022:SlidesScript  
Nov 16, 2022:SlidesScriptNotes 
Nov 17, 2022:SlidesScriptNotes 
Nov 23, 2022:SlidesScriptNotes 
Nov 24, 2022:SlidesScriptNotes 
Nov 30, 2022:SlidesScriptNotes 
Dec 01, 2022:SlidesScript  
Dec 07, 2022:SlidesScript  
Dec 14, 2022:SlidesScriptNotes 
Dec 15, 2022:SlidesScriptNotes 
Dec 21, 2022:SlidesScript  
Dec 22, 2022:SlidesScript  
Jan 04, 2023:Slides Notes 
Jan 05, 2023:SlidesScriptNotes 
Jan 11, 2023:SlidesScriptNotes 
Jan 12, 2023:SlidesScriptNotesSPASS Input PCP
Jan 18, 2023:SlidesScriptNotesArray Theory
Jan 19, 2023:SlidesScriptNotes 
Jan 25, 2023:SlidesScriptNotes 
Jan 26, 2023:SlidesScriptNotes 
Feb 01, 2023:SlidesScriptNotes 
Feb 08, 2023:Slides Notes 


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

Course material from other lectures

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.