Deciding effectively propositional logic using DPLL and substitution sets
This paper introduces a DPLL calculus that is a decision procedure for the Bernays-Schönfinkel class, also called EPR. This class of first-order formulas provides a generalization of pure propositional satisfiablility and quantified Boolean formulas. The presented DPLL calculus is complete in EPR and combines techniques for efficient propositional search, such as Binary Decision Diagrams. The calculus works directly at the level of sets and it is opened up to efficient implementations based on data structures, with promising preliminary empirical results.
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Boolean expression diagrams
- Complexity results for classes of quantificational formulas
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- Deciding effectively propositional logic using DPLL and substitution sets
- 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
- Proof Systems for Effectively Propositional Logic
- Resolution decision procedures
- The model evolution calculus as a first-order DPLL method
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
- SGGS decision procedures
- SCL clause learning from simple models
- A complete and terminating approach to linear integer solving
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
- NRCL -- a model building approach to the Bernays-Schönfinkel fragment
- Ensuring correctness of model transformations while remaining decidable
- Automated reasoning building blocks
- Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
- On the verification of security-aware E-services
- scientific article; zbMATH DE number 2090306 (Why is no real title available?)
- A decidable fragment of second order logic with applications to synthesis
- Feferman-vaught decompositions for prefix classes of first order logic
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Synthesis of distributed agreement-based systems with efficiently-decidable verification
- Exploring partial models with SCL
- Deciding effectively propositional logic using DPLL and substitution sets
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)
