- 2021
- Stephan Gocht, Jakob Nordström, Ruben Martins:
Certifying CNF Encodings of Pseudo-Boolean Constraints (abstract). PxTP 2021: 48 - Maria Paola Bonacina:
Proof Generation in CDSAT. PxTP 2021: 1-4 - Quentin Garchery:
A Framework for Proof-carrying Logical Transformations. PxTP 2021: 5-23 - Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial:
General Automation in Coq through Modular Transformations. PxTP 2021: 24-39 - Hans-Jörg Schurr, Mathias Fleury
, Haniel Barbosa, Pascal Fontaine:
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP 2021: 49-54 - Nicolas Magaud:
Integrating an Automated Prover for Projective Geometry as a New Tactic in the Coq Proof Assistant. PxTP 2021: 40-47 - Chantal Keller, Mathias Fleury:
Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021. EPTCS 336, 2021 [contents] - 2019
- Eunice Palmeira da Silva, Fred Freitas, Jens Otten:
Converting ALC Connection Proofs into ALC Sequents. PxTP 2019: 3-17 - Burak Ekici, Arjun Viswanathan, Yoni Zohar, Clark W. Barrett, Cesare Tinelli:
Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract). PxTP 2019: 18-26 - Mohamed Yacine El Haddad, Guillaume Burel, Frédéric Blanqui:
EKSTRAKTO A tool to reconstruct Dedukti proofs from TSTP files (extended abstract). PxTP 2019: 27-35 - Mathias Fleury, Hans-Jörg Schurr:
Reconstructing veriT Proofs in Isabelle/HOL. PxTP 2019: 36-50 - Fadil Kallat, Tristan Schäfer, Anna Vasileva:
CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories. PxTP 2019: 51-65 - Giselle Reis, Haniel Barbosa:
Proceedings Sixth Workshop on Proof eXchange for Theorem Proving, PxTP 2019, Natal, Brazil, August 26, 2019. EPTCS 301, 2019 [contents] - 2017
- Gilles Dowek:
Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems. PxTP 2017: 3-12 - Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine:
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP 2017: 15-22 - Silvio Ghilardi, Elena Pagani:
Counter Simulations via Higher Order Quantifier Elimination: a preliminary report. PxTP 2017: 39-53 - Tomer Libal, Xaviera Steele:
Determinism in the Certification of UNSAT Proofs. PxTP 2017: 55-76 - Dennis Müller, Colin Rothgang, Yufei Liu, Florian Rabe:
Alignment-based Translations Across Formal Systems Using Interface Theories. PxTP 2017: 77-93 - Robert Y. Lewis:
An Extensible Ad Hoc Interface between Lean and Mathematica. PxTP 2017: 23-37 - Catherine Dubois, Bruno Woltzenlogel Paleo:
Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, PxTP 2017, Brasília, Brazil, 23-24 September 2017. EPTCS 262, 2017 [contents] - 2015
- Ali Assaf, Guillaume Burel:
Translating HOL to Dedukti. PxTP@CADE 2015: 74-88 - Ali Assaf, Raphaël Cauderlier:
Mixing HOL and Coq in Dedukti (Extended Abstract). PxTP@CADE 2015: 89-96 - Mark Adams:
The Common HOL Platform. PxTP@CADE 2015: 42-56 - Christoph Benzmüller, Maximilian Claus, Nik Sultana:
Systematic Verification of the Modal Logic Cube in Isabelle/HOL. PxTP@CADE 2015: 27-41 - Raphaël Cauderlier, Pierre Halmagrand:
Checking Zenon Modulo Proofs in Dedukti. PxTP@CADE 2015: 57-73 - Quentin Heath, Dale Miller:
A framework for proof certificates in finite state exploration. PxTP@CADE 2015: 11-26 - Giselle Reis:
Importing SMT and Connection proofs as expansion trees. PxTP@CADE 2015: 3-10 - Cezary Kaliszyk, Andrei Paskevich:
Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, PxTP 2015, Berlin, Germany, August 2-3, 2015. EPTCS 186, 2015 [contents] - 2013
- Christoph Benzmüller, Nik Sultana:
LEO-II Version 1.5. PxTP@CADE 2013: 2-10 - Jasmin Christian Blanchette:
Redirecting Proofs by Contradiction. PxTP@CADE 2013: 11-26
