Pages that link to "Item:Q5747649"

The following pages link to Fast LCF-Style Proof Reconstruction for Z3 (Q5747649):

Displaying 31 items.

• Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
• Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
• A verified SAT solver framework with learn, forget, restart, and incrementality (Q1663234) (← links)
• Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
• Eliciting implicit assumptions of Mizar proofs by property omission (Q1945901) (← links)
• Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
• Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
• Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
• Pegasus: sound continuous invariant generation (Q2147687) (← links)
• GRUNGE: a grand unified ATP challenge (Q2305410) (← links)
• Extending Sledgehammer with SMT solvers (Q2351158) (← links)
• SMT proof checking using a logical framework (Q2441776) (← links)
• A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (Q2817909) (← links)
• A Complete Decision Procedure for Linearly Compositional Separation Logic with Data Constraints (Q2817951) (← links)
• A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
• An Evaluation of Automata Algorithms for String Analysis (Q3075486) (← links)
• Validating QBF Validity in HOL4 (Q3088005) (← links)
• Proving Valid Quantified Boolean Formulas in HOL Light (Q3088006) (← links)
• LCF-Style Bit-Blasting in HOL4 (Q3088019) (← links)
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
• Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
• Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL (Q3100212) (← links)
• Automatic Proof and Disproof in Isabelle/HOL (Q3172879) (← links)
• Satisfiability Modulo Theories (Q3176369) (← links)
• Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (Q3454099) (← links)
• Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
• A formalization of convex polyhedra based on the simplex method (Q5915783) (← links)
• A formal proof of the expressiveness of deep learning (Q5915784) (← links)
• Scalable fine-grained proofs for formula processing (Q5919479) (← links)
• A formal proof of the expressiveness of deep learning (Q5919583) (← links)
• Pegasus: a framework for sound continuous invariant generation (Q6535946) (← links)