- Referenced in 472 articles
- proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple...
- Referenced in 195 articles
- ground clauses with equality. Then, a decision procedure based on ground equational rewriting is applied...
- Referenced in 108 articles
- 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...
- Referenced in 146 articles
- integration of a linear arithmetic decision procedure and the addition of a rather primitive facility...
- Referenced in 116 articles
- provides an implementation of automaton-based decision procedures for the logics WS1S and WS2S...
- Referenced in 158 articles
- same time BerkMin introduces a new decision-making procedure and a new method of clause...
- Referenced in 94 articles
- core system architecture and decision procedures to take advantage of recent engineering and algorithmic advances...
- Referenced in 47 articles
- 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...
- Referenced in 76 articles
- ting equation to a decision procedure. While CBMC is aimed for embedded software, it also...
- Referenced in 49 articles
- 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...
- Referenced in 58 articles
- interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports...
- Referenced in 37 articles
- Slam, Blast, or Magic use decision procedures for abstraction and simulation that are limited...
- Referenced in 26 articles
- implements the framework of $delta $-complete decision procedures: It returns either unsat or $delta...
- Referenced in 18 articles
- 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...
- Referenced in 25 articles
- based verification. As a stand-alone decision procedure for the theories of uninterpreted functions...
- Referenced in 24 articles
- describe QUBOS (QUantified BOolean Solver), a decision procedure for quantified Boolean logic. The procedure...
- Referenced in 24 articles
- given problem. Darwin is a decision procedure for function-free clause sets...
- Referenced in 23 articles
- important applications in automata theory and decision procedures (validity as well as model checking...
- Referenced in 16 articles
- 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...
- Referenced in 20 articles
- Canonizer and Solver) is an efficient decision procedure for a fragment of first-order logic...