Flexible proof production in an industrial-strength SMT solver

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

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

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

• Coq
• MiniSat
• Isabelle/HOL
• SMT-LIB
• z3
• Sledgehammer
• veriT
• SMTInterpol
• CLSAT
• CVC4
• MathSAT5
• DRAT-trim
• Lean
• SMTCoq
• CertiStr

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