
Bloqqer
 Referenced in 28 articles
[sw09578]
 Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding ... unique and may either introduce variables and clauses not relevant for the solving process ... preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied ... Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques...

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

Boolector
 Referenced in 28 articles
[sw00085]
 Boolector: an efficient SMT solver for bitvectors...

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

MiniSat
 Referenced in 536 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

R
 Referenced in 8601 articles
[sw00771]
 R is a language and environment for statistical...

SCIP
 Referenced in 472 articles
[sw01091]
 SCIP is currently one of the fastest non...

ML
 Referenced in 517 articles
[sw01218]
 ML (’Meta Language’) is a generalpurpose functional...

ALGOL 68
 Referenced in 291 articles
[sw01226]
 ALGOL 68 (short for ALGOrithmic Language 1968) is...

UBCSAT
 Referenced in 36 articles
[sw02614]
 UBCSAT: An implementation and experimentation environment for SLS...

VAMPIRE
 Referenced in 239 articles
[sw02918]
 Vampire 8.0, [RV02,Vor05] is an automatic theorem...

PVS
 Referenced in 620 articles
[sw03484]
 PVS is a verification system: that is, a...

Eiffel
 Referenced in 290 articles
[sw03522]
 Eiffel is an ISOstandardized, objectoriented programming...

CPLEX
 Referenced in 2583 articles
[sw04082]
 IBM® ILOG® CPLEX® offers C, C++, Java, .NET...

SPASS
 Referenced in 178 articles
[sw04108]
 SPASS is an automated theorem prover for first...

TPTP
 Referenced in 378 articles
[sw04143]
 The TPTP (Thousands of Problems for Theorem Provers...

CUDD
 Referenced in 148 articles
[sw04446]
 The CUDD package provides functions to manipulate Binary...

SATO
 Referenced in 196 articles
[sw04451]
 SATO: A Solver for Propositional Satisfiability: The Davis...

z3
 Referenced in 509 articles
[sw04887]
 Z3 is a highperformance theorem prover being...