Skip to Main content Skip to Navigation
Theses

Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve

Abstract : In this thesis, we are interested in the cooperation of first-order rewriting and constructive type theory to improve the automation of computer-aided proofs. We aim to integrate (simple, conditional or AC) rewriting in the Coq proof assistant by an automatic, safe and efficient means using an external programming environment ELAN. Two different approaches are investigated. In the mixed approach, ELAN is used as an external rewriting engine for normalising terms in a reflexive rewriting tactic in Coq. The normalisation trace generated by ELAN is replayed in Coq to compute the corresponding normal form. In order to improve the performance of this reflexive tactic, we show how to use lazy rewriting for producing compact normalisation traces.The second approach called external is more flexible since it also covers several useful extensions of term rewriting such as conditional rewriting and AC rewriting, and it can be easily adapted to other proof assistants. In this approach, term rewriting is entirely performed in ELAN and proof assistants are only used for checking purpose. We formalise the notion of proof term for ELAN computations in the rewriting calculus with explicit substitutions. We investigate the equivalent properties of the proof terms and translate them into the syntax of proof assistant in order to check the corresponding computations. By this work, non-deterministic ELAN computations can be independently certified and we obtain term rewriting in proof assistant. In order to speed up proof-checking of the computations involving AC rewriting, we also propose an efficient method for proving equalities modulo AC based on the syntacticness of AC theories. These results have been integrated in a new ELAN-based rewriting tactic in Coq.
Document type :
Theses
File URL :
http://docnum.univ-lorraine.fr/prive/SCD_T_2002_0144_NGUYEN.pdf
Complete list of metadatas

https://hal.univ-lorraine.fr/tel-01746719
Contributor : Thèses Ul <>
Submitted on : Thursday, March 29, 2018 - 10:43:16 AM
Last modification on : Wednesday, October 14, 2020 - 4:19:01 AM

Identifiers

  • HAL Id : tel-01746719, version 1

Collections

Citation

Quang Huy Nguyen. Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2002. Français. ⟨NNT : 2002NAN10144⟩. ⟨tel-01746719⟩

Share

Metrics

Record views

25