Foundational proof certificates in first-order logic

Zakaria Chihani 1 Dale Miller 1 Fabien Renaud 1
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 : It is the exception that provers share and trust each others proofs. One reason for this is that different provers structure their proof evidence in remarkably different ways, including, for example, proof scripts, resolution refutations, tableaux, Herbrand expansions, natural deductions, etc. In this paper, we propose an approach to foundational proof certificates as a means of flexibly presenting proof evidence so that a relatively simple and universal proof checker can check that a certificate does, indeed, elaborate to a formal proof. While we shall limit ourselves to first-order logic in this paper, we shall not limit ourselves in many other ways. Our framework for defining and checking proof certificates will work with classical and intuitionistic logics and with proof structures as diverse as resolution refutations, matings, and natural deduction.
Type de document :
Communication dans un congrès
CADE - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States. 2013
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00906485
Contributeur : Fabien Renaud <>
Soumis le : mardi 19 novembre 2013 - 20:28:18
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : jeudi 20 février 2014 - 09:45:40

Fichier

root.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00906485, version 1

Collections

Citation

Zakaria Chihani, Dale Miller, Fabien Renaud. Foundational proof certificates in first-order logic. CADE - 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States. 2013. 〈hal-00906485〉

Partager

Métriques

Consultations de la notice

419

Téléchargements de fichiers

128