RISC Logo
    News       Library       Links       Sitemap       Search  
line
 
 Decidable Logical Theories
 

Entry requirements:

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.

Asessment/Examination:

Written or oral exam.

Course aims:

Students should become familiar with the principal decidability results in the area of logical theories and with the basic methods involved, especially quantifier elimination.

Course description:

A logical theory in the most general sense is any set of sentences (of predicate logic), but this course deals specifically with theories T of the following form: for some class K of models, T is the theory of K, that is, the set of all sentences which are satisfied by every model in K. Such theories turn out to be decidable in various cases of interest, and decision algorithms will be given. A number of general approaches 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 certain model-theoretic methods for proving decidability. Chapter 2 deals with the theory of integers with addition (Presburger arithmetic) and related theories; it introduces the 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 the decidability of the theory of some class of algebraic structures carries over to cartesian products and generalized products of such structures; this is used to show the decidability of the theory of abelian groups. In the final chapter 5 the decidability of the theory of Boolean algebras and of linear orderings are shown.

Time and place:

Thursday 9:00-10:30, Seminar Room Schloß Hagenberg

Literature:

Lecture notes will be handed out.
    This page is maintained by Heinrich Rolletschek . Last updated on October 12, 2004