• 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 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...
  • 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 high-level language and interactive...
  • MetiTarski

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