On deciding satisfiability by theorem proving with speculative inferences
From MaRDI portal
Publication:438533
DOI10.1007/s10817-010-9213-yzbMath1243.68265OpenAlexW2150307403WikidataQ118190413 ScholiaQ118190413MaRDI QIDQ438533
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
Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35)
Related Items
Semantically-guided goal-sensitive reasoning: model representation, 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, Rewriting modulo SMT and open system analysis, On First-Order Model-Based Reasoning, Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover, Superposition decides the first-order logic fragment over ground theories, Semantically-guided goal-sensitive reasoning: inference system and completeness, Making theory reasoning simpler, On Interpolation in Decision Procedures, Superposition for Bounded Domains, Theorem Proving in Large Formal Mathematics as an Emerging AI Field, Canonical Ground Horn Theories, Blocking and other enhancements for bottom-up model generation methods, SGGS decision procedures, Larry Wos: visions of automated reasoning, Set of support, demodulation, paramodulation: a historical perspective, On interpolation in automated theorem proving
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- 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
- Theory decision by decomposition
- A rewriting approach to satisfiability procedures.
- Automated model building
- Rewrite-Based Decision Procedures
- Model-based Theory Combination
- Rewrite-Based Satisfiability Procedures for Recursive Data Structures
- Automated complexity analysis based on ordered resolution
- Engineering DPLL(T) + Saturation
- Simplify: a theorem prover for program checking
- Integrating Linear Arithmetic into Superposition Calculus
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- ${\mathcal{T}}$ -Decision by Decomposition
- Blocking and Other Enhancements for Bottom-Up Model Generation Methods
- Decidability and Undecidability Results for Nelson-Oppen and Rewrite-Based Decision Procedures
- Superposition Modulo Linear Arithmetic SUP(LA)
- 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
- Proving termination with multiset orderings
- Simplification by Cooperating Decision Procedures
- Presburger arithmetic with unary predicates is Π11 complete
- An algorithm for finding canonical sets of ground rewrite rules in polynomial time
- Proving refutational completeness of theorem-proving strategies
- Rewrite-based Equational Theorem Proving with Selection and Simplification
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Automated Inference of Finite Unsatisfiability
- A Decision Procedure for Monotone Functions over Bounded and Complete Lattices
- Computer Science Logic
- Automated Deduction – CADE-20
- On Variable-inactivity and Polynomial Formula-Satisfiability Procedures
- On Local Reasoning in Verification
- Frontiers of Combining Systems
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- Computer Aided Verification
- A Decidable Class of Nested Iterated Schemata
- Verification, Model Checking, and Abstract Interpretation
