QE で証明 - ATPとCASのこと

と言えば，やはり不等式の成立です．すなわち

変数が仮定を満たすならば，結論の不等式が成り立つ

という論理式を QE すれば，その式と同値で量化子を含まない式（とくに，成り立つときは true，成り立たないときは false）が得られる（RedLog ではtrue，false の評価は QE を待たず直ちに行われる）のですから，例えば，命題

$x+y+z=0$ を満たす任意の実数 $x,\;y,\;z$ について
$\frac{x(x+2)}{2x^2+1}+\frac{y(y+2)}{2y^2+1}+\frac{z(z+2)}{2z^2+1}\ge0$
が成り立つ

に対して

f[x_] := x (x+ 2)/(2 x^2 + 1);
Reduce[ForAll[{x, y, z}, x + y + z == 0, f[x] + f[y] + f[z] >= 0 ] ]

と QE すれば，Mathematica は，直ちに

True

と答えますし，実数 $c$ の条件

$x+y+z=0$ を満たす任意の実数 $x,\;y,\;z$ について
$\frac{x(x+c)}{cx^2+1}+\frac{y(y+c)}{cy^2+1}+\frac{z(z+c)}{cz^2+1}\ge0$
が成り立つ

に対しても

f[x_] := x (x+ c)/(c x^2 + 1);
Reduce[ForAll[{x, y, z}, x + y + z == 0, f[x] + f[y] + f[z] >= 0 ] ]

と QE すれば，Mathematica は

0 <= c <= 2

と答えます．