• HOL

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

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

  • Referenced in 100 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 136 articles [sw07543]
  • integration of a linear arithmetic decision procedure and the addition of a rather primitive facility...
  • MONA

  • Referenced in 113 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...
  • 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...
  • CVC4

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

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

  • Referenced in 42 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 36 articles [sw12804]
  • Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited...
  • QUBOS

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

  • Referenced in 17 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 23 articles [sw07157]
  • implements the framework of $delta $-complete decision procedures: It returns either unsat or $delta...
  • Darwin

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

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

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

  • Referenced in 15 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 19 articles [sw21618]
  • Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic...