Description

This lecture is part of the elective module "Automated Reasoning". The other parts of the module (the lecture "Computational Logic") is given in the winter term. It is recommended to attend (and pass) the course on logic, before the lecture on automated reasoning is heard, but this is not a requirement.

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

pdf	full lecture notes

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

semantic tableaux	propositonal logic	prolog	first-order logic	prolog
resolution	propositonal logic		first-order logic	prolog