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.

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$$.