Flexible proof production in an industrial-strength SMT solver
type: Item
instance of: scholarly article
title: Flexible proof production in an industrial-strength SMT solver
DOI: 10.1007/978-3-031-10769-6_3
author: Haniel Barbosa
author: Andrew Reynolds
author: Gereon Kremer
author: Hanna Lachnitt
author: Aina Niemetz
author: Andres Nötzli
author: Alex Ozdemir
author: Mathias Preiner
author: Arjun Viswanathan
author: Scott Viteri
author: Yoni Zohar
author: Cesare Tinelli
author: Clark Barrett
publication date: 2022-12-07T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7628179
cites work: DRAT-trim
cites work: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
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: Q5219923
cites work: Satisfiability Modulo Theories
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Extending Sledgehammer with SMT solvers
cites work: Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
cites work: Fast LCF-Style Proof Reconstruction for Z3
cites work: Satisfiability modulo transcendental functions via incremental linearization
cites work: The MathSAT5 SMT Solver
cites work: Construction of Real Algebraic Numbers in Coq
cites work: Efficient certified RAT verification
cites work: The Lean 4 theorem prover and programming language
cites work: Exploiting Symmetry in SMT Problems
cites work: Theory and Applications of Satisfiability Testing
cites work: SMTCoq: a plug-in for integrating SMT solvers into Coq
cites work: A mathematical introduction to logic.
cites work: Tools and Algorithms for the Construction and Analysis of Systems
cites work: Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
cites work: A verified implementation of algebraic numbers in Isabelle/HOL
cites work: Extended resolution simulates \({\mathsf{DRAT}}\)
cites work: Efficient verified (UN)SAT certificate checking
cites work: Implementing the cylindrical algebraic decomposition within the Coq system
cites work: Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
cites work: Solving SAT and SAT Modulo Theories
cites work: Q4823141
cites work: DRAT-based bit-vector proofs in CVC4
cites work: High-level abstractions for simplifying extended string constraints in SMT
cites work: Scaling up DPLL(T) string solvers using context-dependent simplification
cites work: Q4221106
cites work: Reliable reconstruction of fine-grained proofs in a proof assistant
cites work: SMT proof checking using a logical framework
cites work: Algebraic Numbers in Isabelle/HOL
describes a project that uses: DRAT-trim
describes a project that uses: Coq
describes a project that uses: Isabelle/HOL
describes a project that uses: SMT-LIB
describes a project that uses: MathSAT5
describes a project that uses: CVC4
describes a project that uses: MiniSat
describes a project that uses: z3
describes a project that uses: Lean
describes a project that uses: SMTCoq
describes a project that uses: SMTInterpol
describes a project that uses: veriT
describes a project that uses: CertiStr
describes a project that uses: CLSAT
describes a project that uses: Sledgehammer
MaRDI profile type: Publication
full work available at URL: 978-3-031-10769-6 3
OpenAlex ID: W4289104006
description: scientific article; zbMATH DE number 7628179