A Tarski formula is an integral polynomial constraint, i.e. relation(polynom(integer)), truefalse, or a boolean combination of Tarski formulae, where allowable operators are $\mathrm{And}$, $\mathrm{Or}$, $\mathrm{Implies}$, $\mathrm{Xor}$, and $\mathrm{Not}$, or a Tarski formula quantified via $\mathrm{forall}$ or $\mathrm{exists}$.

A Real Tarski formula (RTF) is as above, but with allowable polynomial constraints having real algebraic number coefficients, i.e. relation(polynom(realalgnum)). Real algebraic numbers allow for real algebraic numbers represented by RootOfs indexed by rational intervals.

An Extended Tarski formula (ETF) is as above, but with allowable polynomial constraints being over real algebraic functions. A real algebraic function is a real algebraic number (as realalgnum), or a parametric $\mathrm{RootOf}$ of real algebraic functions with exactly one parameter.

This hence forms a chain of supertypes - a Tarski formula is a subtype of a Real Tarski formula, which is a subtype of an Extended Tarski formula.

A Rational Tarski formula is as one of the above, but the polynomial constraint is instead a constraint on a rational function, where the polynomials in the rational function have realalgnum coefficients, or radnum coefficients convertible to realalgnum coefficients. In other words the coefficients must have the type relation(ratpoly(Or(realalgnum,And(radnum,Not(nonreal)))).

In terms of the QuantifierElimination package:

Tarski formulae are applicable for usage of Virtual Term Substitution (VTS) as an algorithm for Quantifier Elimination (QE). In particular, VTS will not immediately allow for real algebraic numbers.

Real Tarski formulae are applicable for usage of Cylindrical Algebraic Decomposition (CAD), including in QE contexts.

Extended Tarski formulae are never applicable as input for any QuantifierElimination routine, although in practice they may be equivalent to Real Tarski formulae. Extended Tarski formulae may be returned as output for QE when CAD was used as part of QE computation.

Rational Tarski formulae are converted to equivalent Real Tarski formulae before QE computation - see ConvertRationalConstraintsToTarski. In particular, note that Rational Tarski formulae allow for realalgnum coefficients. Radicals (radnums) are also allowable where they are equivalent to a realalgnum - such radicals are converted to their realalgnum counterpart.

The main source of reference for QuantifierElimination and its types can be found in the help page for QuantifierElimination.

$\mathrm{with}\left(\mathrm{QuantifierElimination}\right)\:$$\mathrm{with}\left(\mathrm{QuantifierTools}\right)\:$

$F≔\mathrm{And}\left(x<0\&comma;y<z\right)$

$F≔x<0\wedge y<z$

$\mathrm{type}\left(F\&comma;'\mathrm{TarskiFormula}'\right)$

$\mathrm{true}$

$F≔\mathrm{forall}\left(x\&comma;0<x\Rightarrow 0<x^2\right)$

$F≔\forall \left(x\&comma;0<x\Rightarrow 0<x^2\right)$

$\mathrm{type}\left(F\&comma;'\mathrm{TarskiFormula}'\right)$

$\mathrm{true}$

$F≔\mathrm{RootOf}\left({\mathrm{\_Z}}^2-2\&comma;1..2\right)<x\Rightarrow 1<x$

$F≔\mathrm{RootOf}\left({\mathrm{\_Z}}^2-2\&comma;1..2\right)<x\Rightarrow 1<x$

$\mathrm{type}\left(F\&comma;'\mathrm{RationalTarskiFormula}'\right)$

$\mathrm{true}$

$\mathrm{type}\left(F\&comma;'\mathrm{TarskiFormula}'\right)$

$\mathrm{false}$

$F≔\mathrm{sqrt}\left(2\right)<\frac{x}{y}$

$F≔\sqrt{2}<\frac{x}{y}$

$\mathrm{type}\left(F\&comma;'\mathrm{RationalTarskiFormula}'\right)$

$\mathrm{true}$

$F≔\mathrm{ConvertRationalConstraintsToTarski}\left(F\right)$

$F≔0<-\sqrt{2}{y}^2+yx$

$F≔\mathrm{convert}\left(F\&comma;'\mathrm{RootOf},\mathrm{form}=\mathrm{interval}'\right)$

$F≔0<-\mathrm{RootOf}\left({\mathrm{\_Z}}^2-2\&comma;\frac{1414213557}{1000000000}..\frac{1414213567}{1000000000}\right)y^2+yx$

$\mathrm{type}\left(F\&comma;'\mathrm{RationalTarskiFormula}'\right)$

$\mathrm{true}$