Volume
@proceedings{PxTP2013,
title = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
year = {2013}}
Papers
@inproceedings{PxTP2013:External_Tools_Formal_Proof,
author = {Thomas C. Hales},
title = {External Tools for the Formal Proof of the Kepler Conjecture},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/fPt},
doi = {10.29007/2l48},
pages = {1},
year = {2013}}
@inproceedings{PxTP2013:LEO_II_Version_1.5,
author = {Christoph Benzmüller and Nik Sultana},
title = {LEO-II Version 1.5},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/QJs},
doi = {10.29007/lbxw},
pages = {2-10},
year = {2013}}
@inproceedings{PxTP2013:Redirecting_Proofs_Contradiction,
author = {Jasmin Christian Blanchette},
title = {Redirecting Proofs by Contradiction},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/d6nT},
doi = {10.29007/wm8b},
pages = {11-26},
year = {2013}}
@inproceedings{PxTP2013:From_Classical_Extensional_Higher,
author = {Chad E. Brown and Christine Rizkallah},
title = {From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/Ps},
doi = {10.29007/8p9q},
pages = {27-42},
year = {2013}}
@inproceedings{PxTP2013:Shallow_Embedding_Resolution_Superposition,
author = {Guillaume Burel},
title = {A Shallow Embedding of Resolution and Superposition Proofs into the $\lambda\Pi$-Calculus Modulo},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/jZZS},
doi = {10.29007/ftc2},
pages = {43-57},
year = {2013}}
@inproceedings{PxTP2013:Checking_Foundational_Proof_Certificates,
author = {Zakaria Chihani and Dale Miller and Fabien Renaud},
title = {Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract)},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/WQKh},
doi = {10.29007/7gnr},
pages = {58-66},
year = {2013}}
@inproceedings{PxTP2013:Translating_Higher_Order_Specifications,
author = {Nada Habli and Amy P. Felty},
title = {Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/7c8},
doi = {10.29007/jqtz},
pages = {67-76},
year = {2013}}
@inproceedings{PxTP2013:Initial_Experiments_Deriving_Complete,
author = {Cezary Kaliszyk and Thomas Sternagel},
title = {Initial Experiments on Deriving a Complete HOL Simplification Set},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/h6b},
doi = {10.29007/95qb},
pages = {77-86},
year = {2013}}
@inproceedings{PxTP2013:Stronger_Automation_Flyspeck_Feature,
author = {Cezary Kaliszyk and Josef Urban},
title = {Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/VZv6},
doi = {10.29007/5gzr},
pages = {87-95},
year = {2013}}
@inproceedings{PxTP2013:Extended_Resolution_as_Certificates,
author = {Chantal Keller},
title = {Extended Resolution as Certificates for Propositional Logic},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/Mp3J},
doi = {10.29007/vrpk},
pages = {96-109},
year = {2013}}
@inproceedings{PxTP2013:Challenges_Using_OpenTheory_Transport,
author = {Ramana Kumar},
title = {Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/fbT},
doi = {10.29007/lsnv},
pages = {110-116},
year = {2013}}
@inproceedings{PxTP2013:Robust_Semi_Intelligible_Isabelle,
author = {Steffen Juilf Smolka and Jasmin Christian Blanchette},
title = {Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs},
booktitle = {PxTP 2013. Third International Workshop on Proof Exchange for Theorem Proving},
editor = {Jasmin Christian Blanchette and Josef Urban},
series = {EPiC Series in Computing},
volume = {14},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {/publications/paper/GT},
doi = {10.29007/zbdb},
pages = {117-132},
year = {2013}}
