Redlog Quick Start

Quick Start by Example

Here is a screenshot of an interactive Reduce session, which helps you to quickly get started with Redlog.

Screenshot

About the Example

Recall that quantifier elimination is one of the key concepts in Redlog. Our example in nonlinear real arithmetic illustrates how quantifier elimination solves parametric problems.

Our example has been originally proposed by Hoon Hong. Consider two bivariate polynomials with parameters a and b over the reals: \begin{eqnarray*} f_b(x,y) & = & x^2 + xy + b,\\ g_{a,b}(x,y) & = & x + ay^2 + b. \end{eqnarray*}

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 simultaneously \begin{eqnarray*} f_b(x,y) & > & 0,\\ g_{a,b}(x,y) & \leq & 0. \end{eqnarray*}

This problem can be straightforwardly formulated as a first-order formula: \[\forall x \exists y (x^2 + xy + b > 0 \land x + ay^2 + b \leq 0).\] Redlog's quantifier elimination quickly delivers the necessary and sufficient conditions \(a < 0\) and \(b > 0\).