- Chad E. Brown, Christine Rizkallah:
From Classical Extensional Higher-Order Tableau to Intuitionistic Intentional Natural Deduction. PxTP@CADE 2013: 27-42 - Guillaume Burel:
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo. PxTP@CADE 2013: 43-57 - Zakaria Chihani, Dale Miller, Fabien Renaud:
Checking Foundational Proof Certificates for First-Order Logic (Extended Abstract). PxTP@CADE 2013: 58-66 - Nada Habli, Amy P. Felty:
Translating Higher-Order Specifications to Coq Libraries Supporting Hybrid Proofs. PxTP@CADE 2013: 67-76 - Thomas C. Hales:
External Tools for the Formal Proof of the Kepler Conjecture. PxTP@CADE 2013: 1 - Cezary Kaliszyk, Thomas Sternagel:
Initial Experiments on Deriving a Complete HOL Simplification Set. PxTP@CADE 2013: 77-86 - Cezary Kaliszyk, Josef Urban:
Stronger Automation for Flyspeck by Feature Weighting and Strategy Evolution. PxTP@CADE 2013: 87-95 - Chantal Keller:
Extended Resolution as Certificates for Propositional Logic. PxTP@CADE 2013: 96-109 - Ramana Kumar:
Challenges in Using OpenTheory to Transport Harrison's HOL Model from HOL Light to HOL4. PxTP@CADE 2013: 110-116 - Steffen Juilf Smolka, Jasmin Christian Blanchette:
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs. PxTP@CADE 2013: 117-132 - Jasmin Christian Blanchette, Josef Urban:
Third International Workshop on Proof Exchange for Theorem Proving, PxTP 2013, Lake Placid, NY, USA, June 9-10, 2013. EPiC Series in Computing 14, EasyChair 2013 [contents] - 2012
- Frédéric Besson, Pierre-Emmanuel Cornilleau, Ronan Saillard:
Walking through the Forest: Fast EUF Proof-Checking Algorithms. PxTP 2012: 58-64 - Mathieu Boespflug, Guillaume Burel:
CoqInE: Translating the Calculus of Inductive Constructions into the λΠ-calculus Modulo. PxTP 2012: 44-50 - Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant:
The λΠ-calculus Modulo as a Universal Proof Language. PxTP 2012: 28-43 - Robert L. Constable:
Proof Assistants and the Dynamic Nature of Formal Theories. PxTP 2012: 1-15 - Cvetan Dunchev, Alexander Leitsch, Tomer Libal, Martin Riener, Mikheil Rukhaia, Daniel Weller, Bruno Woltzenlogel Paleo:
System Feature Description: Importing Refutations into the GAPT Framework. PxTP 2012: 51-57 - Stephan Merz:
Proofs and Proof Certification in the TLA+ Proof System. PxTP 2012: 16-20 - Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades III, Corey Oliver, Ruoyu Zhang:
LFSC for SMT Proofs: Work in Progress. PxTP 2012: 21-27 - David Pichardie, Tjark Weber:
Proceedings of the Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. CEUR Workshop Proceedings 878, CEUR-WS.org 2012 [contents] - 2011
- Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie:
A Nelson-Oppen based Proof System using Theory Specific Proof Systems. PxTP 2011: 1-14 - Frédéric Besson, Pascal Fontaine, Laurent Théry:
A Flexible Proof Format for SMT: a Proposal. PxTP 2011: 15-26 - Sascha Böhme, Tjark Weber:
Designing Proof Formats: A User's Perspective. PxTP 2011: 27-32 - David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo:
Quantifier Inference Rules for SMT proofs. PxTP 2011: 33-39 - Stephan Merz, Hernán Vanzetto:
Towards certification of TLA+ proof obligations with SMT solvers. PxTP 2011: 40-45 - Piotr Rudnicki, Josef Urban:
Escape to ATP for Mizar. PxTP 2011: 46-59 - Geoff Sutcliffe, Cynthia Chang, Deborah L. McGuinness, Timothy Lebo, Li Ding, Paulo Pinheiro da Silva:
Combining Proofs to form Different Proofs. PxTP 2011: 60-73 - Pascal Fontaine, Aaron Stump:
PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011. 2011 [contents]
