Presburger arithmetic

Presburger arithmetic is first-order arithmetic over the nonnegative integers with addition, order, and constants, but no multiplication of variables. It is complete and decidable, though its decision procedures have very high complexity.

First-order logic: A formal system in which quantified variables range over objects and predicates express relations among them. Presburger arithmetic uses quantifiers and logical connectives to state its formulas.
Natural number: An element of the nonnegative integers, usually including zero in modern mathematical usage. These are the objects over which Presburger formulas are interpreted.
Peano arithmetic: A first-order theory of the natural numbers with axioms for zero, successor, addition, and multiplication. Unlike Presburger arithmetic, it includes variable multiplication and is incomplete and undecidable.
Mojżesz Presburger: A Polish logician who proved the decidability of first-order arithmetic with addition in 1929. The theory takes its name from his decision result.
Semilinear set: A finite union of sets formed by adding arbitrary nonnegative combinations of fixed integer vectors to fixed base vectors. The integer solutions of Presburger-definable formulas have semilinear structure.
Addition: The arithmetic operation that combines two quantities into their sum. Addition is the only variable-dependent arithmetic operation in the language.
Skolem arithmetic: The first-order theory of natural numbers with multiplication but without addition. It is another decidable arithmetic obtained by retaining a different basic operation.
Entscheidungsproblem: Hilbert's problem of finding a general procedure to decide the validity of mathematical statements. Presburger arithmetic provides a decidable fragment within the broader search for such procedures.
Finite automaton: A finite-state machine that accepts or rejects strings according to transitions between a finite set of states. Automata can recognize encodings of tuples satisfying Presburger formulas.
Linear inequality: An inequality comparing linear expressions whose variables occur only to the first power. Such inequalities express order constraints available in Presburger arithmetic.

Linked from 9 pages