examples

REDLOG Example The following illustrating example has been originally suggested by Hoon Hong: Consider two bivariate polynomials with parameters a and b over the reals: fb(x,y)=x2+xy+b and ga,b(x,y)=x+ay2+b. We are interested in necessary and sufficient conditions on the parameters a and b such that the following holds: For each real point x there exists some real point y such that fb(x,y)>0 and ga,b(x,y)≤0. The problem can be straightforwardly formulated as a first-order formula: φ=∀x∃y(x2+xy+b>0 ∧ x+ay2+b≤0) REDLOG's quantifier elimintion delivers within half a second necessary and sufficient conditions, which are obviously equivalent to a<0 and b>0. A comprehensive collection of REDLOG examples can be found in the REMIS online database.

Click image to enlarge