EasyChair Publications
Search
PxTP 2013 Volume Information
Volume:Jasmin Christian Blanchette and Josef Urban (editors)
PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving

PxTP 2013 Volume Information

Title:PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving
Editors:Jasmin Christian Blanchette and Josef Urban
Series:EPiC Series in Computing
Volume:14
Publication date:May 26, 2013

Papers

AuthorsTitlePagesPDF
Thomas HalesExternal Tools for the Formal Proof of the Kepler Conjecture1
Christoph Benzmüller and Nik SultanaLEO-II Version 1.52-10
Jasmin Christian BlanchetteRedirecting Proofs by Contradiction11-26
Chad Brown and Christine RizkallahFrom Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction27-42
Guillaume BurelA Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo43-57
Zakaria Chihani, Dale Miller and Fabien RenaudChecking Foundational Proof Certificates for First-Order Logic (Extended Abstract)58-66
Nada Habli and Amy FeltyTranslating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs67-76
Cezary Kaliszyk and Thomas SternagelInitial Experiments on Deriving a Complete HOL Simplification Set77-86
Cezary Kaliszyk and Josef UrbanStronger Automation for Flyspeck by Feature Weighting and Strategy Evolution87-95
Chantal KellerExtended Resolution as Certificates for Propositional Logic96-109
Ramana KumarChallenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4110-116
Steffen Juilf Smolka and Jasmin Christian BlanchetteRobust, Semi-Intelligible Isabelle Proofs from ATP Proofs117-132

Keyphrases

CountKeyphrase
7higher order logic
5automatic theorem provers, simple type theory
4hol light
3proof assistants
2analytic tableaux, certificates, flyspeck, isabelle/hol, proof checking, proof theory, resolution, rewriting, sledgehammer, tableaux
1binary decision diagrams, classical, completion, coq, direct proofs, extended resolution, extensional, feature weighting, higher order abstract syntax, hol4, hybrid, intensional, interoperability, intuitionistic, kepler conjecture, large theories, linear programming, machine learning, opentheory, proof transport, prover cooperation, reasoning framework, skolemization, strategy evolution, structured proofs, syntax translation