
KeYmaera
 Referenced in 41 articles
[sw03709]
 complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy...

DISCOVERER
 Referenced in 55 articles
[sw07719]
 polynomial inequalities. Algorithms for quantifier elimination of real closed fields are the general method...

SYNRAC
 Referenced in 28 articles
[sw00942]
 engineering problems. Our main tool is real quantifier elimination and we focus on its application...

MAS
 Referenced in 5 articles
[sw08442]
 exist. MAS further includes algorithms for real quantifier elimination, parametric real root counting...

SACLIB
 Referenced in 25 articles
[sw00823]
 also forms the basis of the quantifier elimination systems QEPCAD [5] and QEPCAD ... with real algebraic numbers [9]; the same routines are also used in quantifier elimination. While...

CGSQE
 Referenced in 2 articles
[sw20574]
 CGSQE/SyNRAC: a real quantifier elimination package based on the computation of comprehensive Gr”obner systems ... CGSQE is a Maple package for real quantifier elimination (QE) we are developing. It works ... given first order formula, CGSQE eliminates all possible quantifiers using the underlying equational constraints ... inequalities of quantified variables, then uses a cylindrical algebraic decomposition based real QE program...

REACH
 Referenced in 4 articles
[sw07733]
 manipulations in number theory, real root isolation, and quantifier elimination. Finally the decision procedures...

TERMINATOR
 Referenced in 3 articles
[sw06692]
 translated to the quantifier elimination problem over the reals, and hence are computable. Finally, feasible...

Vass
 Referenced in 1 article
[sw34696]
 logic/LRA.v: Linear real arithmetic and FourierMotzkin elimination; logic/Presburger.v: Presburger arithmetic and quantifier elimination; algebra...

GUARDIAN
 Referenced in 4 articles
[sw10388]
 cases yielding guarded expressions. We work over real closed fields but our ideas about handling ... detected by simplification and quantifier elimination. Our approach simplifies the expressions on the basis...

DDDLIB
 Referenced in 1 article
[sw00192]
 where $x_1,x_2$ are real variables and $d$ is an integer constant. Formulae ... Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity...

Coq
 Referenced in 1807 articles
[sw00161]
 Coq is a formal proof management system. It...

FGb
 Referenced in 242 articles
[sw00286]
 FGb/Gb libraryGb is a program (191 420 lines...

Isabelle
 Referenced in 611 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Kronecker
 Referenced in 108 articles
[sw00495]
 Kronecker is a package for Magma computer algebra...

Maple
 Referenced in 5124 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 5957 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 12309 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

MetiTarski
 Referenced in 49 articles
[sw00573]
 Many inequalities involving the functions ln, exp, sin...