Automation of Logic
Deutsch

Literature

Automated Reasoning

Script

DateSlidesScriptNotesOther
17.10.2024Slides1Script1  
23.10.2024Slides2   
24.10.2024Slides3Script2  
30.10.2024Slides4   
31.10.2024Slides5   
06.11.2024Slides5Script3  
07.11.2024Slides6   
13.11.2024Slides7 bamboo1 
14.11.2024Slides7   
20.11.2024Sildes7  arXiV
21.11.2024Slides8  Midterm-Layout
27.11.2024Slides9   
28.11.2024Slides10  Midterm-WS2223
     
     
     
     
     
     
     
     
     
     
     
     
     
     

Dictionary

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