Stop the war!
Остановите войну!
for scientists:
default search action
Search dblp for Publications
export results for "stream:conf/pxtp:"
@inproceedings{DBLP:conf/pxtp/GochtNM21, author = {Stephan Gocht and Jakob Nordstr{\"{o}}m and Ruben Martins}, editor = {Chantal Keller and Mathias Fleury}, title = {Certifying {CNF} Encodings of Pseudo-Boolean Constraints (abstract)}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {48}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.5}, doi = {10.4204/EPTCS.336.5}, timestamp = {Thu, 25 Nov 2021 17:17:09 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/GochtNM21.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-02351, author = {Maria Paola Bonacina}, editor = {Chantal Keller and Mathias Fleury}, title = {Proof Generation in {CDSAT}}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {1--4}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.1}, doi = {10.4204/EPTCS.336.1}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-02351.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-02352, author = {Quentin Garchery}, editor = {Chantal Keller and Mathias Fleury}, title = {A Framework for Proof-carrying Logical Transformations}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {5--23}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.2}, doi = {10.4204/EPTCS.336.2}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-02352.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-02353, author = {Valentin Blot and Louise Dubois de Prisque and Chantal Keller and Pierre Vial}, editor = {Chantal Keller and Mathias Fleury}, title = {General Automation in Coq through Modular Transformations}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {24--39}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.3}, doi = {10.4204/EPTCS.336.3}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-02353.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-02354, author = {Hans{-}J{\"{o}}rg Schurr and Mathias Fleury and Haniel Barbosa and Pascal Fontaine}, editor = {Chantal Keller and Mathias Fleury}, title = {Alethe: Towards a Generic {SMT} Proof Format (extended abstract)}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {49--54}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.6}, doi = {10.4204/EPTCS.336.6}, timestamp = {Tue, 07 May 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-02354.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-2107-05493, author = {Nicolas Magaud}, editor = {Chantal Keller and Mathias Fleury}, title = {Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant}, booktitle = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, pages = {40--47}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336.4}, doi = {10.4204/EPTCS.336.4}, timestamp = {Mon, 03 Jan 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-05493.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-2107-01544, editor = {Chantal Keller and Mathias Fleury}, title = {Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021}, series = {{EPTCS}}, volume = {336}, year = {2021}, url = {https://doi.org/10.4204/EPTCS.336}, doi = {10.4204/EPTCS.336}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/abs-2107-01544.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09477, author = {Eunice Palmeira da Silva and Fred Freitas and Jens Otten}, editor = {Giselle Reis and Haniel Barbosa}, title = {Converting {ALC} Connection Proofs into {ALC} Sequents}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {3--17}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.3}, doi = {10.4204/EPTCS.301.3}, timestamp = {Sun, 04 Aug 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09477.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09478, author = {Burak Ekici and Arjun Viswanathan and Yoni Zohar and Clark W. Barrett and Cesare Tinelli}, editor = {Giselle Reis and Haniel Barbosa}, title = {Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {18--26}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.4}, doi = {10.4204/EPTCS.301.4}, timestamp = {Tue, 16 Jul 2024 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09478.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09479, author = {Mohamed Yacine El Haddad and Guillaume Burel and Fr{\'{e}}d{\'{e}}ric Blanqui}, editor = {Giselle Reis and Haniel Barbosa}, title = {{EKSTRAKTO} {A} tool to reconstruct Dedukti proofs from {TSTP} files (extended abstract)}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {27--35}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.5}, doi = {10.4204/EPTCS.301.5}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09479.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09480, author = {Mathias Fleury and Hans{-}J{\"{o}}rg Schurr}, editor = {Giselle Reis and Haniel Barbosa}, title = {Reconstructing veriT Proofs in Isabelle/HOL}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {36--50}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.6}, doi = {10.4204/EPTCS.301.6}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09480.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1908-09481, author = {Fadil Kallat and Tristan Sch{\"{a}}fer and Anna Vasileva}, editor = {Giselle Reis and Haniel Barbosa}, title = {{CLS-SMT:} Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories}, booktitle = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, pages = {51--65}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301.7}, doi = {10.4204/EPTCS.301.7}, timestamp = {Sun, 02 Oct 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-09481.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1908-08639, editor = {Giselle Reis and Haniel Barbosa}, title = {Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019}, series = {{EPTCS}}, volume = {301}, year = {2019}, url = {https://doi.org/10.4204/EPTCS.301}, doi = {10.4204/EPTCS.301}, timestamp = {Sat, 19 Oct 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1908-08639.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-01485, author = {Gilles Dowek}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {3--12}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.1}, doi = {10.4204/EPTCS.262.1}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-01485.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-01486, author = {Haniel Barbosa and Jasmin Christian Blanchette and Simon Cruanes and Daniel El Ouraoui and Pascal Fontaine}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Language and Proofs for Higher-Order {SMT} (Work in Progress)}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {15--22}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.3}, doi = {10.4204/EPTCS.262.3}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-01486.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-01487, author = {Silvio Ghilardi and Elena Pagani}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Counter Simulations via Higher Order Quantifier Elimination: a preliminary report}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {39--53}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.5}, doi = {10.4204/EPTCS.262.5}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-01487.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-01488, author = {Tomer Libal and Xaviera Steele}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Determinism in the Certification of {UNSAT} Proofs}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {55--76}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.6}, doi = {10.4204/EPTCS.262.6}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-01488.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-01489, author = {Dennis M{\"{u}}ller and Colin Rothgang and Yufei Liu and Florian Rabe}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Alignment-based Translations Across Formal Systems Using Interface Theories}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {77--93}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.7}, doi = {10.4204/EPTCS.262.7}, timestamp = {Thu, 14 Oct 2021 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-01489.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/abs-1712-09288, author = {Robert Y. Lewis}, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {An Extensible Ad Hoc Interface between Lean and Mathematica}, booktitle = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, pages = {23--37}, year = {2017}, url = {https://doi.org/10.4204/EPTCS.262.4}, doi = {10.4204/EPTCS.262.4}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-09288.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/abs-1712-00898, editor = {Catherine Dubois and Bruno Woltzenlogel Paleo}, title = {Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Bras{\'{\i}}lia, Brazil, 23-24 September 2017}, series = {{EPTCS}}, volume = {262}, year = {2017}, url = {http://arxiv.org/abs/1712.00898}, timestamp = {Mon, 13 Aug 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/abs-1712-00898.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/0002B15, author = {Ali Assaf and Guillaume Burel}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Translating {HOL} to Dedukti}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {74--88}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.8}, doi = {10.4204/EPTCS.186.8}, timestamp = {Wed, 16 Mar 2022 23:52:32 +0100}, biburl = {https://dblp.org/rec/journals/corr/0002B15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/0002C15, author = {Ali Assaf and Rapha{\"{e}}l Cauderlier}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Mixing {HOL} and Coq in Dedukti (Extended Abstract)}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {89--96}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.9}, doi = {10.4204/EPTCS.186.9}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/0002C15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/Adams15a, author = {Mark Adams}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {The Common {HOL} Platform}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {42--56}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.6}, doi = {10.4204/EPTCS.186.6}, timestamp = {Wed, 12 Sep 2018 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/Adams15a.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/BenzmullerCS15, author = {Christoph Benzm{\"{u}}ller and Maximilian Claus and Nik Sultana}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Systematic Verification of the Modal Logic Cube in Isabelle/HOL}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {27--41}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.5}, doi = {10.4204/EPTCS.186.5}, timestamp = {Wed, 25 Sep 2019 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/BenzmullerCS15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/CauderlierH15, author = {Rapha{\"{e}}l Cauderlier and Pierre Halmagrand}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Checking Zenon Modulo Proofs in Dedukti}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {57--73}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.7}, doi = {10.4204/EPTCS.186.7}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/CauderlierH15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/HeathM15, author = {Quentin Heath and Dale Miller}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {A framework for proof certificates in finite state exploration}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {11--26}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.4}, doi = {10.4204/EPTCS.186.4}, timestamp = {Sat, 09 Apr 2022 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/HeathM15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:journals/corr/Reis15, author = {Giselle Reis}, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Importing {SMT} and Connection proofs as expansion trees}, booktitle = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, pages = {3--10}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186.3}, doi = {10.4204/EPTCS.186.3}, timestamp = {Mon, 28 Aug 2023 01:00:00 +0200}, biburl = {https://dblp.org/rec/journals/corr/Reis15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:journals/corr/KaliszykP15, editor = {Cezary Kaliszyk and Andrei Paskevich}, title = {Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015}, series = {{EPTCS}}, volume = {186}, year = {2015}, url = {https://doi.org/10.4204/EPTCS.186}, doi = {10.4204/EPTCS.186}, timestamp = {Wed, 16 Mar 2022 00:00:00 +0100}, biburl = {https://dblp.org/rec/journals/corr/KaliszykP15.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@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} }
@inproceedings{DBLP:conf/pxtp/BessonCS12, author = {Fr{\'{e}}d{\'{e}}ric Besson and Pierre{-}Emmanuel Cornilleau and Ronan Saillard}, editor = {David Pichardie and Tjark Weber}, title = {Walking through the Forest: Fast {EUF} Proof-Checking Algorithms}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {58--64}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper5.pdf}, timestamp = {Fri, 10 Mar 2023 16:22:21 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BessonCS12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/BoespflugB12, author = {Mathieu Boespflug and Guillaume Burel}, editor = {David Pichardie and Tjark Weber}, title = {CoqInE: Translating the Calculus of Inductive Constructions into the {\(\lambda\)}{\(\Pi\)}-calculus Modulo}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {44--50}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper3.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BoespflugB12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/BoespflugCH12, author = {Mathieu Boespflug and Quentin Carbonneaux and Olivier Hermant}, editor = {David Pichardie and Tjark Weber}, title = {The {\(\lambda\)}{\(\Pi\)}-calculus Modulo as a Universal Proof Language}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {28--43}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper2.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BoespflugCH12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/Constable12, author = {Robert L. Constable}, editor = {David Pichardie and Tjark Weber}, title = {Proof Assistants and the Dynamic Nature of Formal Theories}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {1--15}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/invited1.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/Constable12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/DunchevLLRRWP12, author = {Cvetan Dunchev and Alexander Leitsch and Tomer Libal and Martin Riener and Mikheil Rukhaia and Daniel Weller and Bruno Woltzenlogel Paleo}, editor = {David Pichardie and Tjark Weber}, title = {System Feature Description: Importing Refutations into the {GAPT} Framework}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {51--57}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper4.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/DunchevLLRRWP12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/Merz12, author = {Stephan Merz}, editor = {David Pichardie and Tjark Weber}, title = {Proofs and Proof Certification in the TLA\({}^{\mbox{+}}\) Proof System}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {16--20}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/invited2.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/Merz12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/StumpRTLEOZ12, author = {Aaron Stump and Andrew Reynolds and Cesare Tinelli and Austin Laugesen and Harley Eades III and Corey Oliver and Ruoyu Zhang}, editor = {David Pichardie and Tjark Weber}, title = {{LFSC} for {SMT} Proofs: Work in Progress}, booktitle = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, pages = {21--27}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878/paper1.pdf}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/StumpRTLEOZ12.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/pxtp/2012, editor = {David Pichardie and Tjark Weber}, title = {Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012}, series = {{CEUR} Workshop Proceedings}, volume = {878}, publisher = {CEUR-WS.org}, year = {2012}, url = {https://ceur-ws.org/Vol-878}, timestamp = {Fri, 10 Mar 2023 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/2012.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/BessonCP11, author = {Fr{\'{e}}d{\'{e}}ric Besson and Pierre{-}Emmanuel Cornilleau and David Pichardie}, editor = {Pascal Fontaine and Aaron Stump}, title = {A Nelson-Oppen based Proof System using Theory Specific Proof Systems}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {1--14}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=5}, timestamp = {Thu, 25 Nov 2021 17:51:05 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BessonCP11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/BessonFT11, author = {Fr{\'{e}}d{\'{e}}ric Besson and Pascal Fontaine and Laurent Th{\'{e}}ry}, editor = {Pascal Fontaine and Aaron Stump}, title = {A Flexible Proof Format for {SMT:} a Proposal}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {15--26}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=19}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BessonFT11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/BohmeW11, author = {Sascha B{\"{o}}hme and Tjark Weber}, editor = {Pascal Fontaine and Aaron Stump}, title = {Designing Proof Formats: {A} User's Perspective}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {27--32}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=31}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/BohmeW11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/DeharbeFP11, author = {David D{\'{e}}harbe and Pascal Fontaine and Bruno Woltzenlogel Paleo}, editor = {Pascal Fontaine and Aaron Stump}, title = {Quantifier Inference Rules for {SMT} proofs}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {33--39}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=37}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/DeharbeFP11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/MerzV11, author = {Stephan Merz and Hern{\'{a}}n Vanzetto}, editor = {Pascal Fontaine and Aaron Stump}, title = {Towards certification of {TLA+} proof obligations with {SMT} solvers}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {40--45}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=44}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/MerzV11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/RudnickiU11, author = {Piotr Rudnicki and Josef Urban}, editor = {Pascal Fontaine and Aaron Stump}, title = {Escape to {ATP} for Mizar}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {46--59}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=50}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/RudnickiU11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@inproceedings{DBLP:conf/pxtp/SutcliffeCMLDS11, author = {Geoff Sutcliffe and Cynthia Chang and Deborah L. McGuinness and Timothy Lebo and Li Ding and Paulo Pinheiro da Silva}, editor = {Pascal Fontaine and Aaron Stump}, title = {Combining Proofs to form Different Proofs}, booktitle = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, pages = {60--73}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf\#page=64}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/SutcliffeCMLDS11.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
@proceedings{DBLP:conf/pxtp/2011, editor = {Pascal Fontaine and Aaron Stump}, title = {PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wroc{\l}aw, Poland, August 1, 2011}, year = {2011}, url = {https://pxtp2011.loria.fr/PxTP2011.pdf}, timestamp = {Thu, 25 Nov 2021 00:00:00 +0100}, biburl = {https://dblp.org/rec/conf/pxtp/2011.bib}, bibsource = {dblp computer science bibliography, https://dblp.org} }
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.