Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
type: Item
instance of: scholarly article
title: Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
author: Maria Paola Bonacina
author: Stéphane Graham-Lengrand
author: Natarajan Shankar
published in: Journal of Automated Reasoning
publication date: 2022-03-25T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7498608
zbMATH Keywords: lemma learning
zbMATH Keywords: proof generation
zbMATH Keywords: satisfiability modulo theories
zbMATH Keywords: satisfiability modulo assignment
describes a project that uses: z3
describes a project that uses: LCF
describes a project that uses: Yices
describes a project that uses: Sledgehammer
describes a project that uses: Easychair
MaRDI profile type: Publication
full work available at URL: s10817-021-09606-y
OpenAlex ID: W3199921595
Wikidata QID: Q113901236
cites work: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
cites work: Scalable fine-grained proofs for formula processing
cites work: Extending Sledgehammer with SMT Solvers
cites work: Fast LCF-Style Proof Reconstruction for Z3
cites work: Theory combination: beyond equality sharing
cites work: Conflict-driven satisfiability for theory combination: transition system and completeness
cites work: Interpolation systems for ground proofs in automated deduction: a survey
cites work: On deciding satisfiability by theorem proving with speculative inferences
cites work: Semantically-guided goal-sensitive reasoning: inference system and completeness
cites work: A CDCL-style calculus for solving non-linear constraints
cites work: Linear Integer Arithmetic Revisited
cites work: Q5679729
cites work: Politeness and combination methods for theories with bridging functions
cites work: Natural Domain SMT: A Preliminary Assessment
cites work: Efficient certified RAT verification
cites work: Model-based theory combination
cites work: A Model-Constructing Satisfiability Calculus
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: A comprehensive combination framework
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Solving bitvectors with MCSAT: explanations from bits and pieces
cites work: Verifying Refutations with Extended Resolution
cites work: Inprocessing Rules
cites work: Solving Nonlinear Integer Arithmetic with MCSAT
cites work: Cutting to the chase.
cites work: Solving Non-linear Arithmetic
cites work: Q4051879
cites work: Conflict Resolution
cites work: Decision procedures. An algorithmic point of view. With foreword by Randal E. Bryant
cites work: Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL
cites work: On Fourier's algorithm for linear arithmetic constraints
cites work: Q5503674
cites work: GRASP: a search algorithm for propositional satisfiability
cites work: Generalizing DPLL to Richer Logics
cites work: Q3857731
cites work: Q3677735
cites work: Simplification by Cooperating Decision Procedures
cites work: Solving SAT and SAT Modulo Theories
cites work: Q4221106
cites work: Smoothed analysis of algorithms
cites work: Guarded recursive datatype constructors
cites work: Deciding Bit-Vector Formulas with mcSAT
DOI: 10.1007/S10817-021-09606-Y
description: scientific article; zbMATH DE number 7498608