The following pages link to (Q2848688):
Displaying 13 items.
- Efficiently checking propositional refutations in HOL theorem provers (Q1006729) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Extending Sledgehammer with SMT solvers (Q2351158) (← links)
- Verification of clock synchronization algorithms: experiments on a combination of deductive tools (Q2642981) (← links)
- versat: A Verified Modern SAT Solver (Q2891429) (← 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)
- Linear Arithmetic with Stars (Q3512499) (← links)
- Combining Theories with Shared Set Operations (Q3655212) (← links)
- Extending Sledgehammer with SMT Solvers (Q5200019) (← links)
- Rocket-Fast Proof Checking for SMT Solvers (Q5458346) (← links)
- Scalable fine-grained proofs for formula processing (Q5919479) (← links)
