Skip to Main content Skip to Navigation
Journal articles

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
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.
Document type :
Journal articles
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Dale Miller Connect in order to contact the contributor
Submitted on : Wednesday, November 2, 2016 - 3:50:51 PM
Last modification on : Thursday, January 20, 2022 - 5:27:48 PM
Long-term archiving on: : Friday, February 3, 2017 - 2:15:10 PM


Files produced by the author(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⟩



Les métriques sont temporairement indisponibles