Skip to Main content Skip to Navigation
Conference papers

Certifying Term Rewriting Proof in ELAN

Quang-Huy Nguyen 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Term rewriting has been shown to be a good environment for both programming and proving. We consider the proof term of term rewriting and propose a formalism based on the rewriting calculus with explicit substitutions ($\rho\sigma$-calculus). This formalism is helpful in analysing and in debugging rule-based programs. Moreover, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic term rewriting but also with term rewriting modulo a set of axioms ({\em e.g.} associativity-commutativity).
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00107875
Contributor : Publications Loria <>
Submitted on : Thursday, October 19, 2006 - 9:12:27 AM
Last modification on : Friday, February 26, 2021 - 3:28:06 PM
Long-term archiving on: : Wednesday, March 29, 2017 - 1:33:29 PM

Identifiers

  • HAL Id : inria-00107875, version 1

Collections

Citation

Quang-Huy Nguyen. Certifying Term Rewriting Proof in ELAN. 2nd International Workshop on Rule-based Programming - RULE'01, Sep 2001, Firenze, Italy, 18 p. ⟨inria-00107875⟩

Share

Metrics

Record views

161

Files downloads

82