HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Thursday, October 19, 2006 - 9:12:27 AM
Last modification on : Friday, February 4, 2022 - 3:34:22 AM
Long-term archiving on: : Wednesday, March 29, 2017 - 1:33:29 PM


  • HAL Id : inria-00107875, version 1



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⟩



Record views


Files downloads