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},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340}}
Papers
@inproceedings{PxTP2013:External_Tools_for_Formal,
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},
pages = {1},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/fPt},
doi = {10.29007/2l48}}
@inproceedings{PxTP2013:LEO_II_Version_1.5,
author = {Christoph Benzm\textbackslash{}"uller 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},
pages = {2--10},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/QJs},
doi = {10.29007/lbxw}}
@inproceedings{PxTP2013:Redirecting_Proofs_by_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},
pages = {11--26},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/d6nT},
doi = {10.29007/wm8b}}
@inproceedings{PxTP2013:From_Classical_Extensional_Higher_Order,
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},
pages = {27--42},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/Ps},
doi = {10.29007/8p9q}}
@inproceedings{PxTP2013:Shallow_Embedding_of_Resolution,
author = {Guillaume Burel},
title = {A Shallow Embedding of Resolution and Superposition Proofs into the \textbackslash{}\$\textbackslash{}textbackslash\{\}lambda\textbackslash{}textbackslash\{\}Pi\textbackslash{}\$-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},
pages = {43--57},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/jZZS},
doi = {10.29007/ftc2}}
@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},
pages = {58--66},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/WQKh},
doi = {10.29007/7gnr}}
@inproceedings{PxTP2013:Translating_Higher_Order_Specifications_to,
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},
pages = {67--76},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/7c8},
doi = {10.29007/jqtz}}
@inproceedings{PxTP2013:Initial_Experiments_on_Deriving,
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},
pages = {77--86},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/h6b},
doi = {10.29007/95qb}}
@inproceedings{PxTP2013:Stronger_Automation_for_Flyspeck,
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},
pages = {87--95},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/VZv6},
doi = {10.29007/5gzr}}
@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},
pages = {96--109},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/Mp3J},
doi = {10.29007/vrpk}}
@inproceedings{PxTP2013:Challenges_in_Using_OpenTheory,
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},
pages = {110--116},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/fbT},
doi = {10.29007/lsnv}}
@inproceedings{PxTP2013:Robust_Semi_Intelligible_Isabelle_Proofs,
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},
pages = {117--132},
year = {2013},
publisher = {EasyChair},
bibsource = {EasyChair, https://easychair.org},
issn = {2398-7340},
url = {https://easychair.org/publications/paper/GT},
doi = {10.29007/zbdb}}