Patrick Maier
Decision Procedures for First-order Theories
Dates, Time and Location: Appleton Tower, Room 5.03 on Mondays at 1400-1500 hrs for
8 weeks starting 21 January 2008 - 10 March 2008 inclusive.
Description:In recent years, there has been impressive progress on theorem provers for deciding validity of universal queries in certain first-order theories related to program analysis. The theories covered by these provers are typically combinations of the theories of equality, linear arithmetic (over integers or reals), arrays, etc. However, when one tries to apply these provers to one's own problems, one frequently discovers that they cover just not quite enough; for example, arrays might not be sufficient, one might want to reason about sorted arrays.
The aim of this course is to develop an understanding of how these provers work. We will discuss algorithms for deciding validity in some work-horse theories (propositional logic, linear integer arithmetic, equality). We will also study principles for combining and extending decision procedures (Nelson-Oppen, local theory extensions). The focus of this course is not on efficiency or implementation but on the basic reasoning techniques. Elementary knowledge of first-order logic is required. Reading material will be announced in the course.
The course will be 8 lectures.
Last modified: Tue Oct 9 08:25:55 BST 2007