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},
  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{}textbackslash\{\}lambda\textbackslash{}textbackslash\{\}Pi\textbackslash{}\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}}