PxTP 2013: BibTeX Entries

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}}