Fast LCF-Style Proof Reconstruction for Z3
From MaRDI portal
Publication:5747649
DOI10.1007/978-3-642-14052-5_14zbMath1291.68328OpenAlexW1552715853MaRDI QIDQ5747649
Publication date: 14 September 2010
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-14052-5_14
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (31)
Semi-intelligible Isar proofs from machine-generated proofs ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ Automatic Proof and Disproof in Isabelle/HOL ⋮ Satisfiability Modulo Theories ⋮ Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 ⋮ Pegasus: sound continuous invariant generation ⋮ A verified SAT solver framework with learn, forget, restart, and incrementality ⋮ Hammer for Coq: automation for dependent type theory ⋮ Verified verifying: SMT-LIB for strings in Isabelle ⋮ Eliciting implicit assumptions of Mizar proofs by property omission ⋮ SMT proof checking using a logical framework ⋮ A formalization of convex polyhedra based on the simplex method ⋮ A formal proof of the expressiveness of deep learning ⋮ A formal proof of the expressiveness of deep learning ⋮ Extending Sledgehammer with SMT Solvers ⋮ An Evaluation of Automata Algorithms for String Analysis ⋮ Scalable fine-grained proofs for formula processing ⋮ A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality ⋮ A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints ⋮ Validating QBF Validity in HOL4 ⋮ Proving Valid Quantified Boolean Formulas in HOL Light ⋮ LCF-Style Bit-Blasting in HOL4 ⋮ Reliable reconstruction of fine-grained proofs in a proof assistant ⋮ GRUNGE: a grand unified ATP challenge ⋮ A Survey of Satisfiability Modulo Theory ⋮ A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses ⋮ Modular SMT Proofs for Fast Reflexive Checking Inside Coq ⋮ Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL ⋮ Theorem proving as constraint solving with coherent logic ⋮ Flexible proof production in an industrial-strength SMT solver ⋮ Extending Sledgehammer with SMT solvers
Uses Software
This page was built for publication: Fast LCF-Style Proof Reconstruction for Z3
