výstupy
=======================================================
Quantifier Elimination
in
Elementary Algebra and Geometry
by
Partial Cylindrical Algebraic Decomposition
Version 10 (Interactive)
June 1992
by
Hoon Hong
(hhong@risc.uni-linz.ac.at)
Research Institute for Symbolic Computation
=======================================================
<<QEPCAD>> Enter an informal description between '[' and ']':
[Wendr M2, 1. factor<=0]
<<QEPCAD>> Enter a variable list:
(A,B,TGX,TGY)
<<QEPCAD>> Enter the number of free variables:
2
<<QEPCAD>> Enter a prenex formula:
(A TGX) (A TGY)
[
A + B <= 1 /\
^2 TGX^2 (TGY^2 + 1) + 2 A B TGX TGY ( - TGX TGY + 1) + A TGX^2 (
TGY^2 + 1) + B^2 TGY^2 (TGX^2 + 1) - B TGY^2 (TGX^2 + 1) <= 0
)
]
=======================================================
<<QEPCAD>> Before Normalization>>
finish
=======================================================
An equivalent quantifier-free formula:
[ A <= 0 /\ B >= 0 /\ B + A - 1 <= 0 /\ B + A + 1 >= 0 /\
B - A + 1 >= 0 /\ B - A - 1 <= 0 ]