Preuves des résultats concernant J'ordre de récurrence -Le deuxième cas serait al = 0:2, mais il n'est pas possible ,
5 appliqué à (C.15), on peut déterminer deux cas: -a,[u(t,)]w > a2, p.14 ,
> lY(t,) par ,
2 > art,) par "'2 = a(t1) > art ,
Dans ce cas par le lemme C.5 appliqué à (C.2Ü), on a trois sous-cas : ? al > Q~- Dans ce cas on a 0:1 > art,) par 0:1 >, p.2 ,
Preuves des résultats concernant l'ordre de récurrence ,
Puisque 0:1 ::::: 0:2 -+n o:~ ~ a~, on a : par hypothèse, on a : a ,
2 appliquée à (C.26), on peut déterminer trois cas : -0:1 > o:~ ,
S appliqué à (C.27), on peut déterminer deux sous-cas ,
en reprenant la définition C.2 appliquée à (C.26), on a deux sous-cas * Soit OEl > a~, p.2 ,
28) et a, > o-(t,) (C.3I), donc a ,
S appliqué à (C.27), on peut déterminer deux sous-cas ,
en reprenant la définition C.2 appliquée à (C.26), on a deux sous-cas * Soit QI > a~. Dans ce cas on a oe > o-(t2) par "'1>, pp.2-2 ,
Dans ce cas on a "2 > o-(t2) par, p.2 ,
Abstract, Journal of Functional Programming, vol.34, issue.04, pp.375-416, 1991. ,
DOI : 10.1016/B978-0-12-115350-2.50017-8
Proofby consistency in equational theories, Proceedings 3rd IEEE Symposium on Logic in Computer Science, pp.228-233, 1988. ,
The Lambda-Calculus, its syntax and semantics. Studies in Logic and the Foundation of Mathematics, 1984. ,
Autartik computations in formai proofs, 1997. ,
An overview of ELAN html, Pont-à-Mousson (France), Proceedings of the second International Workshop on Rewriting Logic and Applications, 1998. ,
Automated Mathematical Induction, Journal of Logic and Computation, vol.5, issue.5, pp.631-668, 1995. ,
DOI : 10.1093/logcom/5.5.631
URL : https://hal.archives-ouvertes.fr/inria-00074894
Tiling Transactions in Rewriting Logic, Proceedings of the 4 t h International Workshop on Rewriting Logic and Its Applications, pp.43-62, 2002. ,
DOI : 10.1016/S1571-0661(05)82530-7
Preuves A utomatiques par Récurrence dans les Théories Conditionnelles, Thèse de Doctorat d'Université, 1994. ,
Implicit induction in conditional theories, Journal of Automated Reasoning, vol.31, issue.2, pp.189-235, 1995. ,
DOI : 10.1007/BF00881856
URL : https://hal.archives-ouvertes.fr/inria-00074627
The automation of proofby mathematical induction, Handbook of Automated Reasoning, volume I, chapter 13, pp.845-911, 2001. ,
Confluence properties of weak and strong calculi of explicit substitutions, Journal of the ACM, vol.43, issue.2, 1992. ,
DOI : 10.1145/226643.226675
URL : https://hal.archives-ouvertes.fr/inria-00077189
CiME: Completion modulo E, International Conference on Rewriting Techniques and Applications, pp.416-419, 1996. ,
DOI : 10.1007/3-540-61464-8_70
System Description available at http :f/www ,
Induction=I-Axiomatization+First-Order Consistency, Information and Computation, vol.159, issue.1-2, pp.151-186, 2000. ,
DOI : 10.1006/inco.2000.2875
Induction!ess induction, Handbook of Automated Reasoning, pp.913-962, 2001. ,
Lambda calculus notation with nameless dummies, a too1 for automatic formula manipulation, with application ta the chureh-rosser theorem, Indagationes Mathematicae, vol.34, issue.5, pp.381-392, 1972. ,
Une comparaison d'efficacité entre différents calculs de substitutions explicites, 1997. ,
Sequent calculus viewed modulo, Proceedings of the ESSLLI-2000 Student Session, pp.66-76, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00099056
Orderings for term-rewriting systems, Theoretical Computer Science, vol.17, issue.3, pp.279-301, 1982. ,
DOI : 10.1016/0304-3975(82)90026-3
Theorem proving modulo Rapport de Recherche 3400, Institut National de Recherche en Informatique et en Automatique, 1998. ,
Higher-order unification via explicit substit.utions. Information and Computation, pp.183-235, 2000. ,
DOI : 10.1109/lics.1995.523271
HOL-????: an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol.11, issue.1, pp.21-45, 2001. ,
DOI : 10.1017/S0960129500003236
URL : https://hal.archives-ouvertes.fr/hal-01199524
A rationale for conditional equational programming, Theoretical Computer Science, vol.75, issue.1-2, pp.111-138, 1990. ,
DOI : 10.1016/0304-3975(90)90064-O
Thèse d'habilit.ation, Universit, 1999. ,
Logic for Computer Science: Foundations of Automatic Theorem Proving, volume 5 of Computer Science and Technology Series, 1986. ,
Méthodes pour la Vérification Formelle de systèmes matériels et logiciels à architecture régulière, Thèse de doctorat, 2002. ,
Une extension de l'interprétation de Gôdel à l'analyse et son application à l'éliminat.ion des coupures dans l'analyse et la théorie des types, Second Scandinavian Logic Symposium. Nort.h-Holland, 1970. ,
Interprétation fonctionnelle et élimination des coupures dans l'arithmétique d'ordre supérieur, 1972. ,
Proo]s and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science, 1989. ,
Proofs by induction in equational theories with constructors, Preliminary version in Proceedings 21st Symposium on Foundations of Computer Science, pp.239-266, 1980. ,
DOI : 10.1016/0022-0000(82)90006-X
URL : https://hal.archives-ouvertes.fr/inria-00076533
Induction principles formalized in t.he calculus of const.ruct.ions, Programming of Future Generation Computers : Proceedings of the first Franco-Japanese Symposium on Programming of Future Generation Computers, pp.205-216, 1986. ,
Completion of a Set of Rules Modulo a Set of Equations, Preliminary version in Proceedings llth ACM Symposium on Principles of Programming Languages, pp.1155-1194, 1984. ,
DOI : 10.1137/0215084
Automatic proofs by induction in theories without constructors, Information and Computation, vol.82, issue.1, pp.1-33, 1989. ,
DOI : 10.1016/0890-5401(89)90062-X
Confluence properties of extensional and non-extensional ??-calculi with explicit substitutions (extended abstract), Proceedings of the 7 t h International Conference on Rewriting Techniques and Applications, pp.184-199, 1996. ,
DOI : 10.1007/3-540-61464-8_52
A ??-calculus ?? la de Bruijn with explicit substitutions, Proceedings of the 7'h International Symposium on Programming Language Implementation and Logic Programming, pp.45-62, 1995. ,
DOI : 10.1007/BFb0026813
Generalized ??-reduction and explicit substitutions, Proceedings of the 8 th International Symposium on Programming Language Implementation and Logic Programming, pp.378-392, 1996. ,
DOI : 10.1007/3-540-61756-6_98
Lambda calculus, types and models, 1993. ,
URL : https://hal.archives-ouvertes.fr/cel-00574575
From Àa-ta À v a journey through calculi of explicit substitutions, Proceedings of the 21" Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.60-69, 1994. ,
Typed ??-calculi with explicit substitutions may not terminate, Int. Conf. on Typed Lambda Calculus and Applications, pp.328-334, 1995. ,
DOI : 10.1007/BFb0014062
A sufficient condition for the termination of the direct sum of term rewrite systems, Proceedings of the 4'h annual IEEE Symposium on Logic in Computer Science (LICSS9), pp.396-401, 1989. ,
On proving inductive properties of abstract data types, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '80, pp.154-162, 1980. ,
DOI : 10.1145/567446.567461
Calcul de réécriture et automatisation du raisonnement dans les assistants de preuve, Thèse de doctorat, 2002. ,
A simple proof of sufficient conditions for the termination of the disjoint union of term rewriting systems, Bulletin of the European Association for Theoretical Computer Science, vol.50, pp.223-228, 1993. ,
La science et l'hypothèse, Flammarion, 1902. ,
Complete Sets of Reductions for Some Equational Theories, Journal of the ACM, vol.28, issue.2, pp.233-264, 1981. ,
DOI : 10.1145/322248.322251
Term rewriting induction, Proceedings lOth International Conference on Automated Deduction, pp.162-177, 1990. ,
DOI : 10.1007/3-540-52885-7_86
On termination of the direct sum of term-rewriting systems, Information Processing Letters, vol.26, issue.2, pp.65-70, 1987. ,
DOI : 10.1016/0020-0190(87)90039-1
URL : https://hal.archives-ouvertes.fr/inria-00075874
On the Church-Rosser property for the direct sum of term rewriting systems, Journal of the ACM, vol.34, issue.1, pp.128-143, 1987. ,
DOI : 10.1145/7531.7534
Approche incrémentale des preuves automatiques de terminaison, Thèse de doctorat ,
Rewriting modulo a rewrite system, 1995. ,
Adventures in sequent calculus modulo equations, Electronic Notes in Theoretical Computer Science, vol.15 ,
DOI : 10.1016/S1571-0661(05)82550-2
Preface, Proceedings of the znd International Workshop on Rewriting Logic and its Applications, pp.367-378, 1998. ,
DOI : 10.1016/S1571-0661(05)80022-2
Equational rules for rewriting logic, Theoretical Computer Science, vol.285, issue.2, pp.487-517, 2002. ,
DOI : 10.1016/S0304-3975(01)00366-8
URL : https://doi.org/10.1016/s0304-3975(01)00366-8
Universel Algebra for Computer Scientists, EATCS Monographs on Theoretical Computer Science, vol.25, 1992. ,