• # 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...
• # Vass

• Referenced in 1 article [sw34696]
• logic/LRA.v: Linear real arithmetic and Fourier-Motzkin 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...