Deciding effectively propositional logic using DPLL and substitution sets

DOI10.1007/S10817-009-9161-6MaRDI QIDQ972432zbMATHOpenAlexFDO

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

zbMATH Keywords

SATDPLLBDDSeffectively propositional logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Computer Aided Verification
• scientific article; zbMATH DE number 1931669
• The model evolution calculus.
• The model evolution calculus as a first-order DPLL method

Cites work

• 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

Cited in

(18)

• SGGS decision procedures
• Deciding effectively propositional logic using DPLL and substitution sets
• Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic
• On the verification of security-aware E-services
• Feferman-vaught decompositions for prefix classes of first order logic
• Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• scientific article; zbMATH DE number 2090306 (Why is no real title available?)
• SCL clause learning from simple models
• Automated reasoning building blocks
• Synthesis of distributed agreement-based systems with efficiently-decidable verification
• Ensuring correctness of model transformations while remaining decidable
• Semantically-guided goal-sensitive reasoning: inference system and completeness
• NRCL -- a model building approach to the Bernays-Schönfinkel fragment
• A complete and terminating approach to linear integer solving
• Deciding Effectively Propositional Logic Using DPLL and Substitution Sets
• Decidable \({\exists}^*{\forall}^*\) first-order fragments of linear rational arithmetic with uninterpreted predicates
• scientific article; zbMATH DE number 7533356 (Why is no real title available?)

Describes a project that uses

Uses Software

• MiniSat
• Darwin

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)