- English only

# Lab for Automated Reasoning and Analysis LARA

# Simple QE for Integer Difference Inequalities

## Language of Less-Than-Equals Over Integers

Consider language: and the theory of structure where

**Lemma:** This theory does not admit quantifier elimination.

**Proof.**

Suppose the theory admits quantifier elimination.

**End.**

So must be expressible. Let us extend the language: consider theory in language with interpreted as on integers.

Does the theory of this structure admit quantifier elimination?

## Extending the Language

Language:

Theory of structure where

Note that is the less-than-equal relation on integers.

In other words, we look at the language of this syntax, where is the set of variables:

F ::= A | (F&F) | (F|F) | ~F | ALL V.F | EX V.F A ::= v=v | v + K ≤ v | true | false K ::= ... -2 | -1 | 0 | 1 | 2 | ...

## Quantifier Elimination in the Extended Language

Quantifier elimination for this language is similar to Simple QE for Dense Linear Orders.

What are conjunctions of literals equivalent to?

How do we eliminate existential quantifier?