• QEPCAD

  • Referenced in 255 articles [sw00752]
  • CADs. QEPCAD is an implementation of quantifier elimination by partial cylindrical algebraic decomposition due orginally...
  • SACLIB

  • Referenced in 25 articles [sw00823]
  • also forms the basis of the quantifier elimination systems QEPCAD [5] and QEPCAD ... same routines are also used in quantifier elimination. While runtime-tools such as Valgrind...
  • DISCOVERER

  • Referenced in 35 articles [sw07719]
  • equations and polynomial inequalities. Algorithms for quantifier elimination of real closed fields are the general...
  • KeYmaera

  • Referenced in 30 articles [sw03709]
  • real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool...
  • SYNRAC

  • Referenced in 25 articles [sw00942]
  • problems. Our main tool is real quantifier elimination and we focus on its application...
  • Bloqqer

  • Referenced in 21 articles [sw09578]
  • Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... methods for QBF based on blocked clause elimination ... technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural...
  • Nenofex

  • Referenced in 18 articles [sw09579]
  • this paper is Nenofex, a solver for quantified boolean formulae (QBF) in negation normal form ... eliminating variables. In contrast to eliminating existentially quantified variables by resolution on CNF, which causes...
  • SQEMA

  • Referenced in 33 articles [sw03056]
  • result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula...
  • PASS

  • Referenced in 5 articles [sw21858]
  • quantified expressions that are solved through quantifier elimination. We present an efficient and sound quantifier...
  • Spacer

  • Referenced in 7 articles [sw19496]
  • efficiency depends on an oracle for quantifier elimination (QE). For Boolean programs, the algorithm...
  • f2lp

  • Referenced in 10 articles [sw09898]
  • computing the general language. Quantifiers are first eliminated and then the resulting quantifier-free formulas...
  • MAS

  • Referenced in 5 articles [sw08442]
  • further includes algorithms for real quantifier elimination, parametric real root counting, and for computing...
  • GUARDIAN

  • Referenced in 4 articles [sw10388]
  • detected by simplification and quantifier elimination. Our approach simplifies the expressions on the basis...
  • REACH

  • Referenced in 4 articles [sw07733]
  • number theory, real root isolation, and quantifier elimination. Finally the decision procedures are implemented...
  • Valigator

  • Referenced in 3 articles [sw00994]
  • summation, Gr”obner basis computation, and quantifier elimination. We present general principles of the implementation...
  • TERMINATOR

  • Referenced in 3 articles [sw06692]
  • further be translated to the quantifier elimination problem over the reals, and hence are computable...
  • AIGSolve

  • Referenced in 1 article [sw25923]
  • Inverter Graphs (AIGs). In this approach, quantifiers are eliminated, starting with the inner-most quantifiers ... basic method consists of cofactorbased quantifier elimination which is combined with a multitude of optimization ... based on incremental SAT, heuristics that exchange quantifiers of the same ... level, heuristics that use BDD-based quantifier elimination as an alternative, as well as structure...
  • CGSQE

  • Referenced in 1 article [sw20574]
  • CGSQE/SyNRAC: a real quantifier elimination package based on the computation of comprehensive Gr”obner systems ... Maple package for real quantifier elimination (QE) we are developing. It works cooperating with SyNRAC ... given first order formula, CGSQE eliminates all possible quantifiers using the underlying equational constraints...
  • Theoryguru

  • Referenced in 1 article [sw25572]
  • Theoryguru: a Mathematica package to apply quantifier elimination technology to economics. We consider ... quantifier elimination (QE) technology for automated reasoning in economics. There is a great body...
  • QERRC

  • Referenced in 1 article [sw10387]
  • package QERRC: quantifier elimination...