Flexible proof production in an industrial-strength SMT solver
From MaRDI portal
Publication:2104495
DOI10.1007/978-3-031-10769-6_3OpenAlexW4289104006MaRDI QIDQ2104495
Hanna Lachnitt, Aina Niemetz, Mathias Preiner, Scott Viteri, Gereon Kremer, Andres Nötzli, Yoni Zohar, Cesare Tinelli, Alex Ozdemir, Clark Barrett, Arjun Viswanathan, Andrew Reynolds, Haniel Barbosa
Publication date: 7 December 2022
Full work available at URL: https://doi.org/10.1007/978-3-031-10769-6_3
Related Items (3)
Local Search For Satisfiability Modulo Integer Arithmetic Theories ⋮ Levelwise construction of a single cylindrical algebraic cell ⋮ Verified verifying: SMT-LIB for strings in Isabelle
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- DRAT-trim
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Extended resolution simulates \({\mathsf{DRAT}}\)
- 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
- The Lean 4 theorem prover and programming language
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Scaling up DPLL(T) string solvers using context-dependent simplification
- DRAT-based bit-vector proofs in CVC4
- A verified implementation of algebraic numbers in Isabelle/HOL
- Extending Sledgehammer with SMT solvers
- Satisfiability modulo transcendental functions via incremental linearization
- Efficient certified RAT verification
- SMT proof checking using a logical framework
- Algebraic Numbers in Isabelle/HOL
- Construction of Real Algebraic Numbers in Coq
- 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
- Solving SAT and SAT Modulo Theories
- Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
- Exploiting Symmetry in SMT Problems
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT Solver
- Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
- Theory and Applications of Satisfiability Testing
- Fast LCF-Style Proof Reconstruction for Z3
- Tools and Algorithms for the Construction and Analysis of Systems
- Scalable fine-grained proofs for formula processing
- Efficient verified (UN)SAT certificate checking
- High-level abstractions for simplifying extended string constraints in SMT
This page was built for publication: Flexible proof production in an industrial-strength SMT solver
