Foundational Proof Certificates

Dale Miller 1, 2, *
* Auteur correspondant
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Consider a world where exporting proof evidence into a well defined, universal, and permanent format is taken as "feature zero" for computational logic systems. In such a world, provers will communicate and share theorems and proofs; libraries will archive and organize proofs; and marketplaces of proofs would be open to any prover that admits checkable proof objects. In that world, proof checkers will be the new gatekeepers: they will be entrusted with the task of checking that claimed proof evidence elaborates into a formal proof. Logicians and proof theorists have worked on defining notions of proof that are not based on technology and do not have version numbers attached to them. There are many such proof systems in the literature: Hilbert-Frege proofs, Gentzen's sequent calculus proofs, Prawitz's natural deduction proofs, etc. Each of these proof systems have been given precise syntax and meaning. While such well studied proof descriptions exist, a quick review of the current state of automated and interactive theorem provers reveals that provers seldom output their "proof evidence" using such proof systems. While there is a lot of interest in having provers share and trust each other's proofs most of that work has been based on building bridges between two specific provers: a change in the version number of one prover can cause that bridge to collapse. The ProofCert project has as one of its goals the development of a flexible framework for defining the semantics of a wide range of proof evidence in such a way that provers would define the meaning of their own proof evidence and trusted proof checkers would be able to interpret that meaning and check its formal correctness. To achieve this goal, we must first be able to separate proof evidence from its provenance and then provide a formal and clear framework for defining the semantics of proof evidence. The ProofCert project is focused on the problem of checking formal proof: there is no assumption made that such formal proofs are actually readable by humans.
Type de document :
Chapitre d'ouvrage
David Delahaye and Bruno Woltzenlogel Paleo. All about Proofs, Proofs for All, Mathematical Logic and Foundations (55), College Publications, pp.150-163, 2015, All about Proofs, Proofs for All, 978-1-84890-166-7
Liste complète des métadonnées

https://hal.inria.fr/hal-01239733
Contributeur : Dale Miller <>
Soumis le : mardi 8 décembre 2015 - 10:45:00
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Identifiants

  • HAL Id : hal-01239733, version 1

Citation

Dale Miller. Foundational Proof Certificates. David Delahaye and Bruno Woltzenlogel Paleo. All about Proofs, Proofs for All, Mathematical Logic and Foundations (55), College Publications, pp.150-163, 2015, All about Proofs, Proofs for All, 978-1-84890-166-7. 〈hal-01239733〉

Partager

Métriques

Consultations de la notice

220