Arith.FORALL_ARITH

STRUCTURE

SYNOPSIS

Partial decision procedure for non-existential Presburger natural arithmetic.

DESCRIPTION

FORALL_ARITH_CONV is a partial decision procedure for formulae of Presburger natural arithmetic which are in prenex normal form and have all variables either free or universally quantified. Presburger natural arithmetic is the subset of arithmetic formulae made up from natural number constants, numeric variables, addition, multiplication by a constant, the relations <, <=, =, >=, > and the logical connectives ~, /\, \/, ==>, = (if-and-only-if), ! (‘forall’) and ? (‘there exists’). Products of two expressions which both contain variables are not included in the subset, but the function SUC which is not normally included in a specification of Presburger arithmetic is allowed in this HOL implementation.

Given a formula in the specified subset, the function attempts to prove that it is equal to T (true). The procedure only works if the formula would also be true of the non-negative rationals; it cannot prove formulae whose truth depends on the integral properties of the natural numbers.

FAILURE

The function can fail in two ways. It fails if the argument term is not a formula in the specified subset, and it also fails if it is unable to prove the formula. The failure strings are different in each case.

EXAMPLE

#FORALL_ARITH_CONV "m < SUC m";;
|- m < (SUC m) = T

#FORALL_ARITH_CONV "!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)";;
|- (!m n p q. m <= p /\ n <= q ==> (m + n) <= (p + q)) = T

#FORALL_ARITH_CONV "!m n. ~(SUC (2 * m) = 2 * n)";;
evaluation failed     FORALL_ARITH_CONV -- cannot prove formula

SEEALSO

NEGATE_CONV, EXISTS_ARITH_CONV, ARITH_CONV, ARITH_FORM_NORM_CONV, DISJ_INEQS_FALSE_CONV