-
HOL
- Referenced in 502 articles
[sw05492]
- proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple...
-
Mace4
- Referenced in 202 articles
[sw06905]
- ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied...
-
ELAN
- Referenced in 108 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 149 articles
[sw07543]
- integration of a linear arithmetic decision procedure and the addition of a rather primitive facility...
-
MONA
- Referenced in 118 articles
[sw06170]
- provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S...
-
CVC4
- Referenced in 104 articles
[sw09485]
- core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances...
-
BerkMin
- Referenced in 160 articles
[sw06917]
- same time BerkMin introduces a new decision-making procedure and a new method of clause...
-
CVC
- Referenced in 47 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 77 articles
[sw09719]
- ting equation to a decision procedure. While CBMC is aimed for embedded software, it also...
-
MetiTarski
- Referenced in 49 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 58 articles
[sw12868]
- interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports...
-
SatAbs
- Referenced in 39 articles
[sw12804]
- Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited...
-
PGSolver
- Referenced in 27 articles
[sw14051]
- important applications in automata theory and decision procedures (validity as well as model checking...
-
YAPA
- Referenced in 19 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...
-
dReal
- Referenced in 26 articles
[sw07157]
- implements the framework of $delta $-complete decision procedures: It returns either unsat or $delta...
-
Darwin
- Referenced in 25 articles
[sw04175]
- given problem. Darwin is a decision procedure for function-free clause sets...
-
UCLID
- Referenced in 25 articles
[sw04657]
- based verification. As a stand-alone decision procedure for the theories of uninterpreted functions...
-
QUBOS
- Referenced in 24 articles
[sw09580]
- describe QUBOS (QUantified BOolean Solver), a decision procedure for quantified Boolean logic. The procedure...
-
semprop
- Referenced in 17 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...
-
Cyclist
- Referenced in 20 articles
[sw18519]
- addition, over the years several decision procedures or algorithms have been integrated, focusing on Separation...