Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 2:53:30 PM
Last modification on : Friday, February 4, 2022 - 3:30:57 AM


  • 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⟩



Record views