DISJ_INEQS_FALSE_CONV : conv
STRUCTURE
SYNOPSIS
Proves a disjunction of conjunctions of normalised inequalities is false, provided each conjunction is unsatisfiable.
DESCRIPTION
DISJ_INEQS_FALSE_CONV converts an unsatisfiable normalised arithmetic formula to false. The formula must be a disjunction of conjunctions of less-than-or-equal-to inequalities. The inequalities must have the following form: Each variable must appear on only one side of the inequality and each side must be a linear sum in which any constant appears first followed by products of a constant and a variable. On each side the variables must be ordered lexicographically, and if the coefficient of the variable is 1, the 1 must appear explicitly.
FAILURE
Fails if the formula is not of the correct form or is satisfiable. The function will also fail on certain unsatisfiable formulae due to incompleteness of the procedure used.
EXAMPLE
#DISJ_INEQS_FALSE_CONV
# "(1 * n) <= ((1 * m) + (1 * p)) /\
#  ((1 * m) + (1 * p)) <= (1 * n) /\
#  (5 + (4 * n)) <= ((3 * m) + (1 * p)) \/
#  2 <= 0";;
|- (1 * n) <= ((1 * m) + (1 * p)) /\
   ((1 * m) + (1 * p)) <= (1 * n) /\
   (5 + (4 * n)) <= ((3 * m) + (1 * p)) \/
   2 <= 0 =
   F
SEEALSO
HOL  Kananaskis-14