Skip to main content

The Complexity of the First-Order-Theory of the Integers with Addition


Christoph Haase

Suitable for

MSc in Computer Science
Computer Science, Part B
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C


The goal of this project is to determine the computational complexity of the first-order theory of the integers with addition and equality FO(Z,+,=), but without order. This theory is a strict fragment of Presburger arithmetic, an arithmetic theory that finds numerous applications, for instance, in the verification of infinite-state systems. We aim for making an original scientific contribution by determining what time and space resources are needed in order to decide a sentence in FO(Z,+,=). If time permits, an implementation of the decision procedure developed in this project could be envisioned.

Prerequisites: good familiarity with first-order logic, linear algebra and computational complexity