Keyword:Sledgehammer

Publications
Oracle Integration of Floating-Point Solvers with Isabelle Olle Torstensson and Tjark Weber EasyChair Preprint 8640
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs Steffen Juilf Smolka and Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Redirecting Proofs by Contradiction Jasmin Christian Blanchette In:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving