RG1
Automation of Logic

Script

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
    IOS Press, 2009
  • 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.