The Proof Certifier Checkers

Zakaria Chihani 1 Tomer Libal 1 Giselle Reis 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 : Different theorem provers work within different formalisms and paradigms, and therefore produce various incompatible proof objects. Currently there is a big effort to establish foundational proof certificates (FPC), which would serve as a common " specification language " for all these formats. Such framework enables the uniform checking of proof objects from many different theorem provers while relying on a small and trusted kernel to do so. Checkers is an implementation of a proof checker using foundational proof certificates. By trusting a small kernel based on (focused) sequent calculus on the one hand and by supporting FPC specifications in a prolog-like language on the other hand, it can be used for checking proofs of a wide range of theorem provers. The focus of this paper is on the output of equational resolution theorem provers and for this end, we specify the paramodulation rule. We describe the architecture of Checkers and demonstrate how it can be used to check proof objects by supplying the FPC specification for a subset of the inferences used by E-prover and checking proofs using these inferences.
Type de document :
Communication dans un congrès
Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Sep 2015, Wroclaw, Poland. 9323, pp.201-210, 2015, 〈10.1007/978-3-319-24312-2_14〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01208333
Contributeur : Giselle Reis <>
Soumis le : vendredi 2 octobre 2015 - 14:09:55
Dernière modification le : jeudi 11 janvier 2018 - 01:49:36
Document(s) archivé(s) le : dimanche 3 janvier 2016 - 10:49:29

Fichier

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

Identifiants

Citation

Zakaria Chihani, Tomer Libal, Giselle Reis. The Proof Certifier Checkers. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Sep 2015, Wroclaw, Poland. 9323, pp.201-210, 2015, 〈10.1007/978-3-319-24312-2_14〉. 〈hal-01208333〉

Partager

Métriques

Consultations de la notice

283

Téléchargements de fichiers

105