Proof Certificates for Equality Reasoning

Zakaria Chihani 1 Dale Miller 1, 2
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 : 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
Contributeur : Dale Miller <>
Soumis le : mercredi 2 novembre 2016 - 15:50:51
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14
Document(s) archivé(s) le : vendredi 3 février 2017 - 14:15:10


Fichiers produits par l'(les) auteur(s)



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〉



Consultations de la notice


Téléchargements de fichiers