The Entscheidungsproblem

Contents

The Entscheidungsproblem, proposed by David Hilbert in 1928, refers to the problem of finding a mechanised way of deciding the truth of any given (first order) logical statement. After the notion of algorithms was formalized by Alan Turing and others, this was shown to be impossible, i.e. there is no algorithm for deiciding the validity of any given statement of first order logic.

This has however not deterred researchers, since several interesting fragments of first order logic are still decidable. Hence the Entscheidungsproblem now refers to the problem of classifying classes of formulas as decidable or undecidable. This seminar will be a survey of a few such classes.

The seminars will typically involve presenting some decidable or undecidable class, but also related topics like applications, techniques and historical surveys are of interest. You may propose your own favorite topic if you have one. Some suggested topics include

• Decidable classes: chose from among the known decidable classes.
  • Gödel class
  • Monadic class
  • Maslov class
• Undecidable classes
• Techniques
  • Ordered resolution
• Applications
• Verification of cryptographic protocols
• Tools
  • Spass
  • Otter
  • E

Audience

A basic familiarity with first order logic will be assumed.

Registration

• E. Börger, E. Grädel, Y. Gurevich. The Classical Decision Problem. Springer.

  (Several topics will be taken from this book.)

• W. H. Joyner. Resolution strategies as decision procedures. J. ACM, 23 (3): 398-417, 1976.
• C. G. Fermüller, A. Leitsch, U. Hustadt, T. Tammet. Resolution decision procedures. Handbook of automated reasoning, pages 1791-1849.

  See also PhD thesis of U. Hustadt.

• T. Tammet. Resolution methods for decision problems and finite-model building. PhD Thesis.

Contact