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:

Automated Theorem Provers (including Equality) for First-Order Logic

Resolution and Paramodulation

Application of Automated Theorem Provers for First-Order Logic

Lecture Notes

Lecture Notes (3rd edition, double-sided)

pdf

errata

Additional Material

• Towards an Automatic Analysis of Security Protocols in First-Order Logic
  Christoph Weidenbach
• Neumann-Stubblebine: neustubbG.dfg and neustubbH.dfg
• The SPASS Handbook
• Solution to Robbins Problem
  William McCune

Further Reading

• 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
• First-Order Logic and Automated Theorem Proving
  Melvin Fitting
• The Resolution Calculus
  Alexander Leitsch

Source

• normalform.pl provides a transformation to CNF
• prop_tableau.pl provides simple implementation of propositional tableau
• 1storder_tableau.pl provides simple implementation of free-variable first-order tableau