Flexible proof production in an industrial-strength SMT solver (Q2104495): Difference between revisions

@@ Property / cites work @@
+Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings
+Normal rank
@@ Property / cites work @@
+A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
+Normal rank
@@ Property / cites work @@
+Scalable fine-grained proofs for formula processing
+Normal rank
@@ Property / cites work @@
+Q5219923
@@ Property / cites work: Q5219923 / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Extending Sledgehammer with SMT solvers
@@ Property / cites work: Extending Sledgehammer with SMT solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability modulo transcendental functions via incremental linearization
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Construction of Real Algebraic Numbers in Coq
@@ Property / cites work: Construction of Real Algebraic Numbers in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+The Lean 4 theorem prover and programming language
+Normal rank
@@ Property / cites work @@
+Exploiting Symmetry in SMT Problems
@@ Property / cites work: Exploiting Symmetry in SMT Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Q2703808
@@ Property / cites work: Q2703808 / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors
+Normal rank
@@ Property / cites work @@
+A verified implementation of algebraic numbers in Isabelle/HOL
+Normal rank
@@ Property / cites work @@
+Extended resolution simulates \({\mathsf{DRAT}}\)
@@ Property / cites work: Extended resolution simulates \({\mathsf{DRAT}}\) / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / rank @@
+Normal rank
@@ Property / cites work @@
+Implementing the cylindrical algebraic decomposition within the Coq system
+Normal rank
@@ Property / cites work @@
+Decision Procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Q4823141
@@ Property / cites work: Q4823141 / rank @@
+Normal rank
@@ Property / cites work @@
+DRAT-based bit-vector proofs in CVC4
@@ Property / cites work: DRAT-based bit-vector proofs in CVC4 / rank @@
+Normal rank
@@ Property / cites work @@
+High-level abstractions for simplifying extended string constraints in SMT
+Normal rank
@@ Property / cites work @@
+Scaling up DPLL(T) string solvers using context-dependent simplification
+Normal rank
@@ Property / cites work @@
+Q4221106
@@ Property / cites work: Q4221106 / rank @@
+Normal rank
@@ Property / cites work @@
+Reliable reconstruction of fine-grained proofs in a proof assistant
+Normal rank
@@ Property / cites work @@
+SMT proof checking using a logical framework
@@ Property / cites work: SMT proof checking using a logical framework / rank @@
+Normal rank
@@ Property / cites work @@
+Algebraic Numbers in Isabelle/HOL
@@ Property / cites work: Algebraic Numbers in Isabelle/HOL / rank @@
+Normal rank