Real Quantifier Elimination powered by QEPCAD

Convert logical formulas with rational-coefficient polynomials into equivalent quantifier-free formulas over the reals.

⌘ / Ctrl + Enter to compute

All variables are real. Multiply with *, raise to a power with ^.

Input syntax
Quantifiersexists x: … / forall x, y: …
Comparisons= != < <= > >=
0 < x < 1 is also supported.
Logical operatorsnot, and, or, ->, <->(from strongest to weakest)
Polynomialsx^2 + 2*x*y - 1/3
Integers, decimals, and rational numbers are handled exactly.

The quantifier's : applies to the entire formula on its right. Use parentheses to limit its scope. Symbols such as ∃, ∀, ∧, and ∨ are also supported.

Variable denominators, negative exponents, and functions such as sin and log are not supported.

formula := quantifier | comparison
         | not formula | (formula)
         | formula and/or/->/<-> formula
quantifier := exists/forall vars : formula
comparison := polynomial relation polynomial
Supported formulas and limits

Supports first-order formulas with multiple variables and quantifiers over rational-coefficient polynomials. Free variables can remain in the result.

Limits: 4,000 input characters, 600 tokens, 12 variables after prenex conversion, 64 polynomials, total degree 32, 250 terms per polynomial, and 500 digits per coefficient numerator or denominator. Computations are limited to 60 seconds, 512 MiB of WASM memory, and 1.5 MB of log output. Computations may fail to finish even within these limits. Cancellations and errors are shown separately from truth values.

Result

Not computed
Calculation details
1 / 4