Proof Certificates for Equality Reasoning

Zakaria Chihani 1 Dale Miller 1, 2
1 PARSIFAL - Proof search and reasoning with logic specifications
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
Abstract : The kinds of inference rules and decision procedures that one writes for proofs involving equality and rewriting are rather different from proofs that one might write in first-order logic using, say, sequent calculus or natural deduction. For example, equational logic proofs are often chains of replacements or applications of oriented rewriting and normal forms. In contrast, proofs involving logical connectives are trees of introduction and elimination rules. We shall illustrate here how it is possible to check various equality-based proof systems with a programmable proof checker (the kernel checker) for first-order logic. Our proof checker's design is based on the implementation of focused proof search and on making calls to (user-supplied) clerks and experts predicates that are tied to the two phases found in focused proofs. It is the specification of these clerks and experts that provide a formal definition of the structure of proof evidence. As we shall show, such formal definitions work just as well in the equational setting as in the logic setting where this scheme for proof checking was originally developed. Additionally, executing such a formal definition on top of a kernel provides an actual proof checker that can also do a degree of proof reconstruction. We shall illustrate the flexibility of this approach by showing how to formally define (and check) rewriting proofs of a variety of designs.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2016, 323, pp.93 - 108. 〈10.1016/j.entcs.2016.06.007〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01390919
Contributeur : Dale Miller <>
Soumis le : mercredi 2 novembre 2016 - 15:50:51
Dernière modification le : mercredi 14 novembre 2018 - 16:14:01
Document(s) archivé(s) le : vendredi 3 février 2017 - 14:15:10

Fichier

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

Identifiants

Citation

Zakaria Chihani, Dale Miller. Proof Certificates for Equality Reasoning. Electronic Notes in Theoretical Computer Science, Elsevier, 2016, 323, pp.93 - 108. 〈10.1016/j.entcs.2016.06.007〉. 〈hal-01390919〉

Partager

Métriques

Consultations de la notice

238

Téléchargements de fichiers

88