REAL_LINEAR_PROVER : (thm list * thm list * thm list -> positivstellensatz -> thm) -> thm list * thm list * thm list -> thm

Refute real equations and inequations by linear reasoning (not intended for general use).

The REAL_LINEAR_PROVER function should be given two arguments. The first is a proof translator that constructs a contradiction from a tuple of three theorem lists using a Positivstellensatz refutation, which is essentially a representation of how to add and multiply equalities or inequalities chosen from the list to reach a trivially false equation or inequality such as &0 > &0. The second argument is a triple of theorem lists, respectively a list of equations of the form A_i |- p_i = &0, a list of non-strict inequalities of the form B_j |- q_i >= &0, and a list of strict inequalities of the form C_k |- r_k > &0, with both sides being real in each case. Any theorems not of that form will not lead to an error, but will be ignored and cannot contribute to the proof. The prover attempts to construct a Positivstellensatz refutation by normalization as in REAL_POLY_CONV then linear inequality reasoning, and if successful will apply the translator function to this refutation to obtain D |- F where all assumptions D occurs among the A_i, B_j or C_k. Otherwise, or if the translator itself fails, the call fails.

Fails if there is no refutation using linear reasoning or if an improper form inhibits proof for other reasons, or if the translator fails.

This is not intended for general use. The core real inequality reasoner REAL_ARITH is implemented by:
In this way, all specifically linear functionality is isolated in REAL_LINEAR_PROVER, and the rest of the infrastructure of Positivstellensatz proof translation and initial normalization (including elimination of abs, max, min, conditional expressions etc.) is available for use with more advanced nonlinear provers. Such a prover, based on semidefinite programming and requiring support of an external SDP solver to find Positivstellensatz refutations, can be found in Examples/