External rewriting for skeptical proof assistants

Quang-Huy Nguyen 1 Claude Kirchner 1 Hélène Kirchner 1
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper presents the design, the implementation and experiments of the integration of syntactic, conditional possibly associative-commutative term rewriting into proof assistants based on constructive type theory. Our approach is called external since it consists in performing term rewriting in a specific and efficient environment and to check the computations later in a proof assistant. Two typical systems are considered in this work, ELAN, based on the rewriting calculus, as the term rewriting based environment, and Coq, based on the calculus of inductive constructions as the proof assistant. We first formalise the proof terms for deduction by rewriting and strategies in ELAN using the rewriting calculus with explicit substitutions. We then show how these proof terms can soundly be translated into Coq-syntax where they can be directly type checked. For the method to be applicable for rewriting modulo associativity and commutativity, we provide an effective method to prove equalities modulo these axioms in Coq using ELAN. These results have been integrated into an ELAN based rewriting tactic in Coq.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2002, 29 (3-4), pp.309-336
Liste complète des métadonnées

Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:53:30
Dernière modification le : samedi 26 mai 2018 - 01:17:47


  • HAL Id : inria-00101009, version 1


Quang-Huy Nguyen, Claude Kirchner, Hélène Kirchner. External rewriting for skeptical proof assistants. Journal of Automated Reasoning, Springer Verlag, 2002, 29 (3-4), pp.309-336. 〈inria-00101009〉



Consultations de la notice