• HOL

• Referenced in 455 articles [sw05492]
• proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple...

• Mace4

• Referenced in 185 articles [sw06905]
• ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied...

• ELAN

• Referenced in 101 articles [sw02179]
• logic programming languages, constraints solvers and decision procedures and to offer a modular framework ... logic programming languages, constraints solvers and decision procedures and to offer a modular framework...

• NQTHM

• Referenced in 138 articles [sw07543]
• integration of a linear arithmetic decision procedure and the addition of a rather primitive facility...

• MONA

• Referenced in 114 articles [sw06170]
• provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S...

• BerkMin

• Referenced in 158 articles [sw06917]
• same time BerkMin introduces a new decision-making procedure and a new method of clause...

• CVC4

• Referenced in 84 articles [sw09485]
• core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances...

• CVC

• Referenced in 45 articles [sw09462]
• cooperating validity checker. Decision procedures for decidable logics and logical theories have proven ... describes the CVC (“Cooperating Validity Checker”) decision procedure. CVC implements a framework for combining subsidiary ... decision procedures for certain logical theories into a decision procedure for the theories’ union. Subsidiary ... decision procedures for theories of arrays, inductive datatypes, and linear real arithmetic are currently implemented...

• CBMC

• Referenced in 73 articles [sw09719]
• ting equation to a decision procedure. While CBMC is aimed for embedded software, it also...

• MetiTarski

• Referenced in 43 articles [sw00573]
• prover (Metis) modified to call a decision procedure (QEPCAD) for the theory of real closed ... fields. The decision procedure simplifies clauses by deleting literals that are inconsistent with other algebraic...

• FOCI

• Referenced in 57 articles [sw12868]
• interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports...

• SatAbs

• Referenced in 37 articles [sw12804]
• Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited...

• dReal

• Referenced in 26 articles [sw07157]
• implements the framework of $delta $-complete decision procedures: It returns either unsat or $delta...

• YAPA

• Referenced in 18 articles [sw02739]
• relations: deducibility and static equivalence. Several decision procedures have been proposed for these relations under ... implemented so far. We provide a generic procedure for deducibility and static equivalence that takes ... algorithm covers all the existing decision procedures for convergent theories. We also provide an efficient...

• QUBOS

• Referenced in 24 articles [sw09580]
• describe QUBOS (QUantified BOolean Solver), a decision procedure for quantified Boolean logic. The procedure...

• UCLID

• Referenced in 24 articles [sw04657]
• based verification. As a stand-alone decision procedure for the theories of uninterpreted functions...

• Darwin

• Referenced in 23 articles [sw04175]
• given problem. Darwin is a decision procedure for function-free clause sets...

• PGSolver

• Referenced in 23 articles [sw14051]
• important applications in automata theory and decision procedures (validity as well as model checking...

• semprop

• Referenced in 16 articles [sw28383]
• Lemma and model caching in decision procedures for quantified Boolean formulas. The increasing role ... many applications calls for practically efficient decision procedures. One of the most promising paradigms...

• ICS

• Referenced in 20 articles [sw21618]
• Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic...