On deciding satisfiability by theorem proving with speculative inferences
From MaRDI portal
Publication:438533
DOI10.1007/S10817-010-9213-YzbMATH Open1243.68265OpenAlexW2150307403WikidataQ118190413 ScholiaQ118190413MaRDI QIDQ438533FDOQ438533
Leonardo de Moura, Christopher Lynch, Maria Paola Bonacina
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9213-y
Recommendations
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- An Abstract Framework for Satisfiability Modulo Theories
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- SMELS: satisfiability modulo equality with lazy superposition
- Foundations of satisfiability modulo theories
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Cites Work
- Simplify: a theorem prover for program checking
- Lazy satisfiability modulo theories
- Simplification by Cooperating Decision Procedures
- Proving termination with multiset orderings
- Orderings for term-rewriting systems
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- A Machine-Oriented Logic Based on the Resolution Principle
- Title not available (Why is that?)
- Title not available (Why is that?)
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- A rewriting approach to satisfiability procedures.
- Automated model building
- Rewrite-based satisfiability procedures for recursive data structures
- Engineering DPLL(T) + Saturation
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Presburger arithmetic with unary predicates is Π11 complete
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- Title not available (Why is that?)
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- On Local Reasoning in Verification
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Paramodulation-based theorem proving
- Superposition modulo linear arithmetic SUP(LA)
- Theory decision by decomposition
- Rewrite-based decision procedures
- Model-based theory combination
- Automated complexity analysis based on ordered resolution
- Integrating Linear Arithmetic into Superposition Calculus
- ${\mathcal{T}}$ -Decision by Decomposition
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Combinations of Theories for Decidable Fragments of First-Order Logic
- Data structures with arithmetic constraints: A non-disjoint combination
- Combining theories with shared set operations
- Automated Inference of Finite Unsatisfiability
- A Decision Procedure for Monotone Functions over Bounded and Complete Lattices
- Computer Science Logic
- Automated Deduction – CADE-20
- Automated reasoning in some local exensions of ordered structures
- Frontiers of Combining Systems
- Title not available (Why is that?)
- A Decidable Class of Nested Iterated Schemata
- Towards a foundation of completion procedures as semidecision procedures
- A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
- Theorem-proving with resolution and superposition
- On word problems in Horn theories
Cited In (21)
- Blocking and other enhancements for bottom-up model generation methods
- Larry Wos: visions of automated reasoning
- Set of support, demodulation, paramodulation: a historical perspective
- Quantifier simplification by unification in SMT
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
- Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations
- Theorem Proving in Large Formal Mathematics as an Emerging AI Field
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Semantically-guided goal-sensitive reasoning: model representation
- Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover
- Towards a Semantics of Unsatisfiability Proofs with Inprocessing
- On First-Order Model-Based Reasoning
- Making theory reasoning simpler
- QSMA: A New Algorithm for Quantified Satisfiability Modulo Theory and Assignment
- Rewriting modulo SMT and open system analysis
- Canonical Ground Horn Theories
- Superposition decides the first-order logic fragment over ground theories
- On interpolation in automated theorem proving
- Superposition for Bounded Domains
- On Interpolation in Decision Procedures
- SGGS decision procedures
Uses Software
This page was built for publication: On deciding satisfiability by theorem proving with speculative inferences
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q438533)
