Deciding effectively propositional logic using DPLL and substitution sets
From MaRDI portal
Publication:972432
DOI10.1007/S10817-009-9161-6zbMATH Open1197.03011OpenAlexW1999468161MaRDI QIDQ972432FDOQ972432
Authors: Ružica Piskač, Leonardo de Moura, Nikolaj Bjørner 
Publication date: 26 May 2010
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-009-9161-6
Recommendations
Cites Work
- Theory and Applications of Satisfiability Testing
- Graph-Based Algorithms for Boolean Function Manipulation
- The model evolution calculus as a first-order DPLL method
- Resolution decision procedures
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Proof Systems for Effectively Propositional Logic
- Lemma Learning in the Model Evolution Calculus
- Geometric Resolution: A Proof Procedure Based on Finite Model Search
- Deciding effectively propositional logic using DPLL and substitution sets
- Complexity results for classes of quantificational formulas
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Theory and Applications of Satisfiability Testing
- Boolean expression diagrams
- Encodings of Bounded LTL Model Checking in Effectively Propositional Logic
- Programming Languages and Systems
Cited In (18)
- Feferman-vaught decompositions for prefix classes of first order logic
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- On the verification of security-aware E-services
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- Title not available (Why is that?)
- Ensuring Correctness of Model Transformations While Remaining Decidable
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Deciding effectively propositional logic using DPLL and substitution sets
- SCL clause learning from simple models
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment
- Synthesis of distributed agreement-based systems with efficiently-decidable verification
- A complete and terminating approach to linear integer solving
- Automated Reasoning Building Blocks
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Title not available (Why is that?)
- SGGS decision procedures
Uses Software
This page was built for publication: Deciding effectively propositional logic using DPLL and substitution sets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q972432)
