Search dblp for Publications

export results for "toc:db/conf/cade/pxtp2013.bht:"

 download as .bib file

@inproceedings{DBLP:conf/cade/BenzmullerS13,
  author       = {Christoph Benzm{\"{u}}ller and
                  Nik Sultana},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {{LEO-II} Version 1.5},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {2--10},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/lbxw},
  doi          = {10.29007/LBXW},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/BenzmullerS13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Blanchette13,
  author       = {Jasmin Christian Blanchette},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Redirecting Proofs by Contradiction},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {11--26},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/wm8b},
  doi          = {10.29007/WM8B},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Blanchette13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/BrownR13,
  author       = {Chad E. Brown and
                  Christine Rizkallah},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {From Classical Extensional Higher-Order Tableau to Intuitionistic
                  Intentional Natural Deduction},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {27--42},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/8p9q},
  doi          = {10.29007/8P9Q},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/BrownR13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Burel13,
  author       = {Guillaume Burel},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {A Shallow Embedding of Resolution and Superposition Proofs into the
                  {\(\lambda\)}{\(\Pi\)}-Calculus Modulo},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {43--57},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/ftc2},
  doi          = {10.29007/FTC2},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Burel13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/ChihaniMR13a,
  author       = {Zakaria Chihani and
                  Dale Miller and
                  Fabien Renaud},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Checking Foundational Proof Certificates for First-Order Logic (Extended
                  Abstract)},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {58--66},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/7gnr},
  doi          = {10.29007/7GNR},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/ChihaniMR13a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/HabliF13,
  author       = {Nada Habli and
                  Amy P. Felty},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Translating Higher-Order Specifications to Coq Libraries Supporting
                  Hybrid Proofs},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {67--76},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/jqtz},
  doi          = {10.29007/JQTZ},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/HabliF13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Hales13,
  author       = {Thomas C. Hales},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {External Tools for the Formal Proof of the Kepler Conjecture},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {1},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/2l48},
  doi          = {10.29007/2L48},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Hales13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/KaliszykS13,
  author       = {Cezary Kaliszyk and
                  Thomas Sternagel},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Initial Experiments on Deriving a Complete {HOL} Simplification Set},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {77--86},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/95qb},
  doi          = {10.29007/95QB},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/KaliszykS13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/KaliszykU13a,
  author       = {Cezary Kaliszyk and
                  Josef Urban},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Stronger Automation for Flyspeck by Feature Weighting and Strategy
                  Evolution},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {87--95},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/5gzr},
  doi          = {10.29007/5GZR},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/KaliszykU13a.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Keller13,
  author       = {Chantal Keller},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Extended Resolution as Certificates for Propositional Logic},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {96--109},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/vrpk},
  doi          = {10.29007/VRPK},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Keller13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/Kumar13,
  author       = {Ramana Kumar},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Challenges in Using OpenTheory to Transport Harrison's {HOL} Model
                  from {HOL} Light to {HOL4}},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {110--116},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/lsnv},
  doi          = {10.29007/LSNV},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/Kumar13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{DBLP:conf/cade/SmolkaB13,
  author       = {Steffen Juilf Smolka and
                  Jasmin Christian Blanchette},
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Robust, Semi-Intelligible Isabelle Proofs from {ATP} Proofs},
  booktitle    = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  pages        = {117--132},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://doi.org/10.29007/zbdb},
  doi          = {10.29007/ZBDB},
  timestamp    = {Sun, 15 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/SmolkaB13.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@proceedings{DBLP:conf/cade/2013pxtp,
  editor       = {Jasmin Christian Blanchette and
                  Josef Urban},
  title        = {Third International Workshop on Proof Exchange for Theorem Proving,
                  PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013},
  series       = {EPiC Series in Computing},
  volume       = {14},
  publisher    = {EasyChair},
  year         = {2013},
  url          = {https://easychair.org/publications/volume/PxTP\_2013},
  timestamp    = {Fri, 13 Aug 2021 01:00:00 +0200},
  biburl       = {https://dblp.org/rec/conf/cade/2013pxtp.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}
a service of  Schloss Dagstuhl - Leibniz Center for Informatics

manage site settings

To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.