Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems

Gilles Dowek
(Inria and École Normale Supérieure de Paris-Saclay)

We describe the first results of a project of analyzing in which theories formal proofs can be ex- pressed. We use this analysis as the basis of interoperability between proof systems.

Invited Speaker in Catherine Dubois and Bruno Woltzenlogel Paleo: Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving (PxTP 2017), Brasília, Brazil, 23-24 September 2017, Electronic Proceedings in Theoretical Computer Science 262, pp. 3–12.
Published: 4th December 2017.
ArXived at: https://dx.doi.org/10.4204/EPTCS.262.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org