Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
From MaRDI portal
Publication:3541720
DOI10.1007/978-3-540-71070-7_35zbMath1165.03320OpenAlexW2168613335MaRDI QIDQ3541720
Nikolaj Bjørner, Leonardo de Moura
Publication date: 27 November 2008
Published in: Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_35
Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)
Related Items (10)
versat: A Verified Modern SAT Solver ⋮ Semantically-guided goal-sensitive reasoning: model representation ⋮ On the verification of security-aware E-services ⋮ SMT proof checking using a logical framework ⋮ Mu-calculus satisfiability with arithmetic constraints ⋮ Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning ⋮ Deciding effectively propositional logic using DPLL and substitution sets ⋮ A Slice-Based Decision Procedure for Type-Based Partial Orders ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq
Cites Work
- Unnamed Item
- Complexity results for classes of quantificational formulas
- The model evolution calculus as a first-order DPLL method
- Automated deduction -- CADE-21. 21st international conference on automated deduction, Bremen, Germany, July 17--20, 2007. Proceedings
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Proof Systems for Effectively Propositional Logic
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Graph-Based Algorithms for Boolean Function Manipulation
- Lemma Learning in the Model Evolution Calculus
- Programming Languages and Systems
- Theory and Applications of Satisfiability Testing
This page was built for publication: Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
