Thursday, 10:15-11:45 K 112A beginning October 4.
Acquaintance with the most common algebraic structures (groups, lattices etc.); basic knowledge of predicate logic. Results beyond the basics will be given in the lecture.
Students should become familiar with the principal decidability results in the area of logical theories and with the basic methods involved, especially quantifier elimination.
This course deals with one important aspect of automated theorem proving. Let K be some class of algebraic structures (models), for instance, the class of all groups or linear orderings, or the class consisting only of the field of real numbers. The question arises if there exists an algorithm for deciding whether or not a given sentence ϕ belongs to the theory of K, that is, whether or not ϕ is satisfied by every model in K. The answer is negative in general, but in several cases of interest a decision algorithm does indeed exist and will be developed in the lecture. A number of general techniques will be introduced, the most important being quantifier elimination.
Chapter 1 uses some very simple logical theories to illustrate the basic method of quantifier elimination, as well as model-theoretic methods for proving decidability. Chapter 2 deals with the theory of integers with addition (Presburger arithmetic) and related theories; it introduces the general method of Ehrenfeucht games. Chapter 3 deals with the theories of algebraically closed and real closed fields; the latter is one of the most famous examples of a decidable logical theory, and many algorithm have been developed in the past. Chapter 4 shows how a decidability result for some class of algebraic structures carries over to cartesian products and generalized products; this allows to show the decidability of the theory of abelian groups. In the final Chapter 5 the decidability of the theories of Boolean algebras and of linear orderings are shown.
Lecture notes will be handed out.