RegularChains[SemiAlgebraicSetTools]
RepresentingQuantifierFreeFormula
return the quantifier-free formula of a parametric box or a regular semi-algebraic system
Calling Sequence
Parameters
Description
Examples
RepresentingQuantifierFreeFormula(pbx)
RepresentingQuantifierFreeFormula(rsas, R)
pbx
-
a parametric box
rsas
a regular semi-algebraic system
R
a polynomial ring
The command RepresentingQuantifierFreeFormula(pbx) returns the representing quantifier-free formula of the parametric box pbx.
The command RepresentingQuantifierFreeFormula(rsas, R) returns the representing quantifier-free formula of the regular semi-algebraic system rsas.
See the page SemiAlgebraicSetTools for the definition of a regular semi-algebraic system and that of a parametric box.
with⁡RegularChains:
with⁡ParametricSystemTools:
with⁡SemiAlgebraicSetTools:
R≔PolynomialRing⁡x,b,a,c
R≔polynomial_ring
F≔a⁢x2+b⁢x+c
N≔
P≔x
H≔a
rrc≔RealRootClassification⁡F,,x,a,3,2,R
rrc≔regular_semi_algebraic_set,border_polynomial
rsas≔rrc11
rsas≔regular_semi_algebraic_set
pbx≔RepresentingBox⁡rsas,R
pbx≔parametric_box
IsParametricBox⁡pbx
true
qff≔RepresentingQuantifierFreeFormula⁡pbx
qff≔quantifier_free_formula
Info⁡qff,R
c,a,b,4⁢a⁢c−b2,−1,−1,1,−1,1,1,−1,−1
F≔a⁢x2+b⁢x+c=0,0<x,a≠0
R≔PolynomialRing⁡x,c,b,a
out≔LazyRealTriangularize⁡F,R,output=list
out≔regular_semi_algebraic_system
map⁡Display,out,R
a⁢x2+b⁢x+c=0x>0−4⁢c⁢a+b2>0andb<0andc>0anda≠0or−4⁢c⁢a+b2>0andb>0andc>0anda<0or−4⁢c⁢a+b2>0andb>0andc<0anda≠0or−4⁢c⁢a+b2>0andb<0andc<0anda>0
P≔PositiveInequalities⁡out1,R
rc≔RepresentingChain⁡out1,R;Display⁡rc,R
rc≔regular_chain
a⁢x2+b⁢x+c=0a≠0
qff≔RepresentingQuantifierFreeFormula⁡out1;Display⁡qff,R
−4⁢c⁢a+b2>0andb<0andc>0anda≠0
or−4⁢c⁢a+b2>0andb>0andc>0anda<0
or−4⁢c⁢a+b2>0andb>0andc<0anda≠0
or−4⁢c⁢a+b2>0andb<0andc<0anda>0
Display⁡out1,R
See Also
LazyRealTriangularize
PositiveInequalities
RealRootClassification
RealTriangularize
RegularChains
RepresentingChain
RepresentingRootIndex
Download Help Document