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

SACLIB
 Referenced in 23 articles
[sw00823]
 also forms the basis of the quantifier elimination systems QEPCAD [5] and QEPCAD ... same routines are also used in quantifier elimination. While runtimetools such as Valgrind...

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

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

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

Bloqqer
 Referenced in 10 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...

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

Nenofex
 Referenced in 10 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...

f2lp
 Referenced in 8 articles
[sw09898]
 computing the general language. Quantifiers are first eliminated and then the resulting quantifierfree formulas...

MAS
 Referenced in 4 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...

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

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

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

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

DDDLIB
 Referenced in 1 article
[sw00192]
 Boolean operators (conjunction, disjunction, negation, etc.), eliminating quantifiers, and deciding functional properties (satisfiability, validity...

ToyElim
 Referenced in 3 articles
[sw09900]
 without these operators. Tasks like elimination of Boolean quantifiers, computation of uniform interpolants, certain forms ... computational processing of logics by operator elimination. The current implementation is basically a toy system...

Lingva
 Referenced in 3 articles
[sw13645]
 program properties using the recently introduced symbol elimination method. We present implementation details and report ... experiments show that Lingva can automatically generate quantified invariants, possibly with alternation of quantifiers, over...

Beaver
 Referenced in 5 articles
[sw00071]
 Beaver: Engineering an efficient SMT solver for bit...

Boolector
 Referenced in 9 articles
[sw00085]
 Satisfiability Modulo Theories (SMT) is the problem of...