Decidable Logical Theories

This course presents decision algorithms for a number of logical theories; among the most important are: the theory of integers with addition, of rational numbers with addition, the theory of real closed and of algebraically closed fields, the theory of abelian groups and of linear orderings. The most important methods for the development of such algorithms are quantifier elimination and Ehrenfeucht games; moreover, model-theoretic method can oftern be used to prove decidability, although they are not particularly suitable for designing algorithms.

The knowledge of computability theory is not assumed as a prerequisite, and no proof methods typical for that theory are used. This means in particular that no undecidability results are shown, and no results which assert lower bounds for the complexity of decision problems.

No textbook corresponds to this course, but the following literature is recommended:

Ferrante/Rackoff: The computational Complexity of Logical Theories. Springer Lecture Notes in Mathematics 78.

Ershov et. at: Elementary Theories. Russian Mathematical Surveys 20 (1965), p. 35-105.