Automated Theorem Proving

Description

This lecture is part of the elective module "Automated Reasoning". The lecture introduces the concepts of automated theorem proving. The following topics will be discussed in the course:

Lecture Notes

• Lecture Notes The lecture notes are here available online.

  Literature

  The course is partly based on the following references
  • The Resolution Calculus
    Alexander Leitsch
  • First-Order Logic and Automated Theorem Proving
    Melvin Fitting
  • Equational Reasoning in Saturation-Based Theorem Proving
    Leo Bachmair and Harald Ganzinger
  • Towards an Automatic Analysis of Security Protocols in First-Order Logic
    Christoph Weidenbach
  • Solution to Robbins Problem
    William McCune

  Additional Material

  • G.S. Boolos, J.P. Burgess, and R.C. Jeffrey
    Computability and Logic
    Cambridge University Press, 2007
    ISBN 978-0-521-87752-7 (hardback)
  • H.-D. Ebbinghaus, J. Flum, and W. Thomas
    Einführung in die mathematische Logik
    Spektrum Akademischer Verlag, 2007
    ISBN 978-3-8274-1691-9
    NB: There is an english translation entitled "Mathematical Logic" of this text book. However this edition is slightly out of date
  • Neumann-Stubblebine: neustubbG.dfg and neustubbH.dfg
  • The SPASS Handbook

  Prototypes

  propositional semantic tableaux:	prolog
  first-order semantic tableaux:	prolog
  first-order resolution:	java (by M. Häusler)	prolog	haskell (by A. Kochesser)	haskell (by M. Schaper)