Publication:2848688
From MaRDI portal
zbMath1272.68362MaRDI QIDQ2848688
Sean McLaughlin, Clark Barrett, Yeting Ge
Publication date: 26 September 2013
Full work available at URL: http://www.sciencedirect.com/science/article/pii/S1571066106000065
Related Items
Extending Sledgehammer with SMT Solvers, Rocket-Fast Proof Checking for SMT Solvers, Scalable fine-grained proofs for formula processing, Efficiently checking propositional refutations in HOL theorem provers, Reliable reconstruction of fine-grained proofs in a proof assistant, Extending Sledgehammer with SMT solvers, Verification of clock synchronization algorithms: experiments on a combination of deductive tools, versat: A Verified Modern SAT Solver, 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, Linear Arithmetic with Stars, Combining Theories with Shared Set Operations
Uses Software