Stop the war!Остановите войну!
for scientists:
default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDSearch dblp for Publications
export results for "stream:conf/pxtp:"
download as .bib file
@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 = {Mon, 28 Aug 2023 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 = {Sat, 30 Sep 2023 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}
}
a service of 
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.
retrieved on 2024-07-14 01:26 CEST from data curated by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
