Skip to Main content Skip to Navigation

Système de preuve modulo récurrence

Abstract : Methods and systems for proof by induction are very different. The most general methods are difficult to automatize. Automated systems are sometimes difficult to justify.This thesis establishes at proof level a link between noetherian induction and induction bt rewriting, which will enable systems to cooperate in a skeptical mode in which the proof is verified thanks to the Curry-Howard isomorphism.The formalism of deduction modulo is extended to conditional congruences which are evaluated with respect to a context. Moreover,the induction ordering, which cannot be compatible with the congruence, is made protective, which means that it blocks the application of the congruence.Proof by induction by rewriting is seen as the result of the internalization of induction hypotheses in deduction modulo, which enables to explain some of the behavior of the induction by rewriting method.
Document type :
Complete list of metadata

Cited literature [68 references]  Display  Hide  Download
Contributor : Thèses UL Connect in order to contact the contributor
Submitted on : Friday, March 30, 2018 - 9:46:16 AM
Last modification on : Saturday, October 16, 2021 - 11:26:09 AM


Files produced by the author(s)


  • HAL Id : tel-01754351, version 1



Eric Deplagne. Système de preuve modulo récurrence. Autre [cs.OH]. Université Henri Poincaré - Nancy 1, 2002. Français. ⟨NNT : 2002NAN10240⟩. ⟨tel-01754351⟩



Record views


Files downloads