default search action
PxTP@CADE 2013: Lake Placid, NY, USA
- Jasmin Christian Blanchette, Josef Urban:
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013. EPiC Series in Computing 14, EasyChair 2013 - Thomas C. Hales:
External Tools for the Formal Proof of the Kepler Conjecture. 1 - Christoph Benzmüller, Nik Sultana:
LEO-II Version 1.5. 2-10 - Jasmin Christian Blanchette:
Redirecting Proofs by Contradiction. 11-26 - Chad E. Brown, Christine Rizkallah:
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. 27-42 - Guillaume Burel:
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. 43-57 - Zakaria Chihani, Dale Miller, Fabien Renaud:
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). 58-66 - Nada Habli, Amy P. Felty:
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. 67-76 - Cezary Kaliszyk, Thomas Sternagel:
Initial Experiments on Deriving a Complete HOL Simplification Set. 77-86 - Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. 87-95 - Chantal Keller:
Extended Resolution as Certificates for Propositional Logic. 96-109 - Ramana Kumar:
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. 110-116 - Steffen Juilf Smolka, Jasmin Christian Blanchette:
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. 117-132
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.