PxTP@CADE

Keyphrases

Publications

2015

volume 186, 2015

Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. PxTP@CADE 186 (2015)

2013

Thomas C. Hales
External Tools for the Formal Proof of the Kepler Conjecture. PxTP@CADE (2013)
Steffen Juilf Smolka, Jasmin Christian Blanchette
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. PxTP@CADE (2013)
Ramana Kumar
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. PxTP@CADE (2013)
Chantal Keller
Extended Resolution as Certificates for Propositional Logic. PxTP@CADE (2013)
Nada Habli, Amy P. Felty
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. PxTP@CADE (2013)
Jasmin Christian Blanchette
Redirecting Proofs by Contradiction. PxTP@CADE (2013)
Cezary Kaliszyk, Thomas Sternagel
Initial Experiments on Deriving a Complete HOL Simplification Set. PxTP@CADE (2013)
Cezary Kaliszyk, Josef Urban
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE (2013)
Guillaume Burel
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. PxTP@CADE (2013)
Zakaria Chihani, Dale Miller, Fabien Renaud
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). PxTP@CADE (2013)
Christoph Benzmüller, Nik Sultana
LEO-II Version 1.5. PxTP@CADE (2013)
Chad E. Brown, Christine Rizkallah
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. PxTP@CADE (2013)

volume 14, 2013

Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013 PxTP@CADE 14 (2013)