SKEDSOFT

Presburger formulas: The basic terms in Presburger arithmetic consist of first-order variables x, y, x1, x , . . ., the constants 0, and 1, and sums of basic terms. For instance, x x 1 1 1 is a basic term, which we also write as 2x 3. The atomic formulas are equalities and inequalities between basic terms. For instance, x 2y = 3z 1 is an atomic formula. The formulas of Presburger logic are first-order formulas built on the atomic formulas. For instance,
∀x.∃y.(x = 2y ∨ x = 2y 1)
is a formula. The free variables of formula ϕ are defined as usual: for instance,
FV (ϕ1 ∨ ϕ2) = FV (ϕ1) ∪ FV (ϕ2), and FV (∃x.ϕ) = FV (ϕ) \ {x}.
A formula without free variables is called a sentence. Sentences are true (valid) or false (non-valid). Any first-order formula with nested quantifiers, for example
∀x.(p(x) ⇒ [∃y.q(x, y)])
may be rewritten as a logically equivalent formula, in this example as
∀x.∃y.[p(x) ⇒ q(x, y)]
using a transformation process called prenexing or arriving at the prenex normal form. As another example, the prenex normal form for the formula
∀x.([∃y.q(x, y)] ⇒ p(x))

is
∀x.∀y.[q(x, y) ⇒ p(x)].
Notice how the quantifier changes from ∃ to ∀ when lifted out of the antecedent of an implication, since the antecedent of an implication has an implicit negation (a ⇒ b is equivalent to ¬a ∨ b). After prenexing, we are left with a list of quantified variables called the prefix and a quantifier-free inner formula called the matrix. While prenexing is not essential in the Presburger formula to DFA transformation to be described, it is quite helpful for the purposes of exposition. Another
reason why we present prenexing is that it is an important algorithm to know about. The full set of rewrite rules for prenexing are captured in the Ocaml program in Figure 20.1.
The interpretation domain of formulas is the set of natural numbers Nat in which 0, 1, , =, and ≤ have their usual meanings. A solution of a formula is an assignment of the free variables of the formula in Nat which satisfies the formula.