Analyzing Individual Proofs as the Basis of Interoperability between Proof Systems
Gilles Dowek (Inria, \'Ecole Normale Sup\'erieure de Paris-Saclay)
TL;DR
This paper explores how analyzing individual proofs can facilitate interoperability between different proof systems by identifying common formal structures.
Contribution
It introduces a novel approach to analyze proofs for enabling interoperability across various proof systems.
Findings
Initial analysis of proof theories conducted
Framework for proof interoperability proposed
Potential for cross-system proof sharing demonstrated
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Formal Methods in Verification · Logic, Reasoning, and Knowledge