Pages that link to "Item:Q3100209"
From MaRDI portal
The following pages link to A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209):
Displaying 21 items.
- Automating Boolean set operations in Mizar proof checking with the aid of an external SAT solver (Q286803) (← links)
- Semi-intelligible Isar proofs from machine-generated proofs (Q287340) (← links)
- Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs (Q832719) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- FoCaLiZe and Dedukti to the rescue for proof interoperability (Q1687726) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- SMT-based generation of symbolic automata (Q2182674) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- SMT proof checking using a logical framework (Q2441776) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- A Survey of Satisfiability Modulo Theory (Q2830018) (← links)
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq (Q3100210) (← links)
- Tactics for Reasoning Modulo AC in Coq (Q3100211) (← links)
- Proving Correctness of a KRK Chess Endgame Strategy by Using Isabelle/HOL and Z3 (Q3454099) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- SAT-Enhanced Mizar Proof Checking (Q5495946) (← links)
- A formalization of convex polyhedra based on the simplex method (Q5915783) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
