Fast LCF-Style Proof Reconstruction for Z3
From MaRDI portal
Recommendations
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Fast zeta transforms for lattices with few irreducibles
- Fast Zeta Transforms for Lattices with Few Irreducibles
- Fast congruence closure and extensions
- Accelerating tableaux proofs using compact representations
- Efficient lattice-based polynomial evaluation and batch ZK arguments
- Scalable LCF-style proof translation
- Efficient algorithms for Zeckendorf arithmetic
- Unbounded Proof-Length Speed-Up in Deduction Modulo
Cited in
(37)- A verified SAT solver framework with learn, forget, restart, and incrementality
- Hammer for Coq: automation for dependent type theory
- Eliciting implicit assumptions of Mizar proofs by property omission
- Reliable reconstruction of fine-grained proofs in a proof assistant
- Theorem proving as constraint solving with coherent logic
- Flexible proof production in an industrial-strength SMT solver
- Pegasus: sound continuous invariant generation
- GRUNGE: a grand unified ATP challenge
- Extending Sledgehammer with SMT solvers
- SMT proof checking using a logical framework
- A verified SAT solver framework with learn, forget, restart, and incrementality
- A complete decision procedure for linearly compositional separation logic with data constraints
- A survey of satisfiability modulo theory
- Integrating a SAT solver with an LCF-style theorem prover
- Semi-intelligible Isar proofs from machine-generated proofs
- An Evaluation of Automata Algorithms for String Analysis
- Validating QBF Validity in HOL4
- Proving Valid Quantified Boolean Formulas in HOL Light
- LCF-style bit-blasting in HOL4
- 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
- Automatic proof and disproof in Isabelle/HOL
- Satisfiability modulo theories
- Proving correctness of a KRK chess endgame strategy by using Isabelle/HOL and Z3
- Extending Sledgehammer with SMT solvers
- A formal proof of the expressiveness of deep learning
- Scalable fine-grained proofs for formula processing
- A formal proof of the expressiveness of deep learning
- Verified verifying: SMT-LIB for strings in Isabelle
- Hammering Floating-Point Arithmetic
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format
- Pegasus: a framework for sound continuous invariant generation
- Reconstruction of SMT proofs with Lambdapi
- Certainty in formalising SMT-LIB for strings in Isabelle
- Interoperability of proof systems with SC-TPTP
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs
This page was built for publication: Fast LCF-Style Proof Reconstruction for Z3
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5747649)
