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).
Type de document :
Communication dans un congrès
2nd International Workshop on Rule-based Programming - RULE'01, Sep 2001, Firenze, Italy, Elsevier Science Publishers, 59/4 (4), 18 p, 2001, Electronic Notes in Theoretical Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00107875
Contributeur : Publications Loria <>
Soumis le : jeudi 19 octobre 2006 - 09:12:27
Dernière modification le : jeudi 11 janvier 2018 - 06:19:57
Document(s) archivé(s) le : mercredi 29 mars 2017 - 13:33:29

Identifiants

  • 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, Elsevier Science Publishers, 59/4 (4), 18 p, 2001, Electronic Notes in Theoretical Computer Science. 〈inria-00107875〉

Partager

Métriques

Consultations de la notice

119

Téléchargements de fichiers

44