Flexible proof production in an industrial-strength SMT solver
From MaRDI portal
Publication:2104495
DOI10.1007/978-3-031-10769-6_3OpenAlexW4289104006MaRDI QIDQ2104495FDOQ2104495
Authors: Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, Clark Barrett 
Publication date: 7 December 2022
Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_3
Cites Work
- Theory and Applications of Satisfiability Testing
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- DRAT-trim
- The MathSAT5 SMT Solver
- Theory and Applications of Satisfiability Testing
- A mathematical introduction to logic.
- Title not available (Why is that?)
- Solving SAT and SAT Modulo Theories
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Extending Sledgehammer with SMT solvers
- SMT proof checking using a logical framework
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
- Satisfiability Modulo Theories
- Implementing the cylindrical algebraic decomposition within the Coq system
- Fast LCF-Style Proof Reconstruction for Z3
- Tools and Algorithms for the Construction and Analysis of Systems
- Efficient verified (UN)SAT certificate checking
- Title not available (Why is that?)
- Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- DRAT-based bit-vector proofs in CVC4
- Efficient certified RAT verification
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
- Title not available (Why is that?)
- Scalable fine-grained proofs for formula processing
- Exploiting Symmetry in SMT Problems
- Construction of Real Algebraic Numbers in Coq
- Satisfiability modulo transcendental functions via incremental linearization
- Algebraic Numbers in Isabelle/HOL
- Extended resolution simulates \({\mathsf{DRAT}}\)
- The Lean 4 theorem prover and programming language
- Scaling up DPLL(T) string solvers using context-dependent simplification
- A verified implementation of algebraic numbers in Isabelle/HOL
- High-level abstractions for simplifying extended string constraints in SMT
Cited In (7)
- Levelwise construction of a single cylindrical algebraic cell
- Verified verifying: SMT-LIB for strings in Isabelle
- Local Search For Satisfiability Modulo Integer Arithmetic Theories
- A resolution-based interactive proof system for UNSAT
- Towards bit-width-independent proofs in SMT solvers
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Making \(\mathsf{IP}=\mathsf{PSPACE}\) practical: efficient interactive protocols for BDD algorithms
Uses Software
This page was built for publication: Flexible proof production in an industrial-strength SMT solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2104495)
