Certifying Term Rewriting Proof in ELAN
Résumé
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).