inria-00107864, version 1
ELAN for equational reasoning in Coq
2nd Workshop on Logical Frameworks & Metalanguage - LFM'00 (2000) 14 p
Abstract: We describe an interface between \textsf{Coq}, an interactive theorem-prover based on type theory and \textsf{ELAN}, an automated deduction system based on rewriting logic. Our objective is to provide efficient tools to implement decision procedures using equational reasoning in \textsf{Coq}. \textsf{ELAN} is used as a rewrite engine. Reflection is used in \textsf{Coq} to translate back the delegated rewrite computations. A rewriting trace is returned from \textsf{ELAN} and replayed in \textsf{Coq}. Correctness is ensured by this replaying which builds a complete proof-term.
- a – INRIA
- 1:
- INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- Domain : Computer Science/Other
- Keywords : proof assistant – equational reasoning – term rewriting – reflection || assistante de preuve – raisonnement équationnel – réécriture – réflexion
- Internal note : A00-R-462 || nguyen00a
- Comment : ISBN 2-7261-1166-1. Colloque avec actes et comité de lecture. internationale.
- inria-00107864, version 1
- http://hal.inria.fr/inria-00107864
- oai:hal.inria.fr:inria-00107864
- From:
- Submitted on: Thursday, 19 October 2006 09:12:09
- Updated on: Friday, 20 October 2006 15:32:31
Export