- English only

# Lab for Automated Reasoning and Analysis LARA

# Definition of Presburger Arithmetic

## Minimalistic Language of Presburger Arithmetic

Consider and consider as the set of all interpretations with domain where is interpreted as addition of natural numbers (these interpretations differ only in values for free variables. This is one definition of Presburger arithmetic over natural numbers.

This theory is very simple to describe, but it is very far from allowing quantifier-elimination. For example, it does not have a name for zero, so we cannot express . It also does not have a way to express .

## Language of Presburger Arithmetic that Admits QE

We look at the theory of integers with addition.

- introduce constant for each integer constant
- introduce not only addition but also subtraction
- to conveniently express certain expressions, introduce function for each , to be interpreted as multiplication by a constant, . We write as
- to enable quantifier elimination from introduce for each predicate (divisibility by constant)

The resulting language