Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
From MaRDI portal
Publication:832719
DOI10.1007/s10817-021-09606-yOpenAlexW3199921595WikidataQ113901236 ScholiaQ113901236MaRDI QIDQ832719
Stéphane Graham-Lengrand, Natarajan Shankar, Maria Paola Bonacina
Publication date: 25 March 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-021-09606-y
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Interpolation systems for ground proofs in automated deduction: a survey
- On deciding satisfiability by theorem proving with speculative inferences
- On Fourier's algorithm for linear arithmetic constraints
- Semantically-guided goal-sensitive reasoning: inference system and completeness
- Edinburgh LCF. A mechanized logic of computation
- Solving bitvectors with MCSAT: explanations from bits and pieces
- A CDCL-style calculus for solving non-linear constraints
- Theory combination: beyond equality sharing
- Politeness and combination methods for theories with bridging functions
- Conflict-driven satisfiability for theory combination: transition system and completeness
- Cutting to the chase.
- Efficient certified RAT verification
- Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
- Deciding Bit-Vector Formulas with mcSAT
- Model-based Theory Combination
- Solving Non-linear Arithmetic
- Inprocessing Rules
- A Model-Constructing Satisfiability Calculus
- Guarded recursive datatype constructors
- Solving Nonlinear Integer Arithmetic with MCSAT
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Conflict Resolution
- Linear Integer Arithmetic Revisited
- Solving SAT and SAT Modulo Theories
- Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
- Natural Domain SMT: A Preliminary Assessment
- Generalizing DPLL to Richer Logics
- Simplification by Cooperating Decision Procedures
- GRASP: a search algorithm for propositional satisfiability
- Verifying Refutations with Extended Resolution
- Smoothed analysis of algorithms
- Extending Sledgehammer with SMT Solvers
- A comprehensive combination framework
- Fast LCF-Style Proof Reconstruction for Z3
- Tools and Algorithms for the Construction and Analysis of Systems
- Scalable fine-grained proofs for formula processing
