Preuves par récurrence : stratégies et résultats de décidabilité

Francis Alexandre 1
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Nous présentons des stratégies pour prouver des formules implicatives. L'objectif principal est de prouver qu'une formule implicative est valide dans le plus petit modèle de Herbrand d'un programme défini donné. Les stratégies présentées utilisent des règles basées sur le pliage et le dépliage. Des classes particulères de formules, les formules bi-implicatives et des classes particulières de programmes, les programmes descendants sont mis en évidence. Pour ces classes on montre que le pliage préserve l'équivalence et qu'il est possible d'étendre certaines classes décidables de programmes. Enfin nous définissons une stratégie de preuve qui peut s'appliquer à une large classe de programmes.
Type de document :
Rapport
[Interne] A02-R-489 || alexandre02c, 2002
Liste complète des métadonnées

https://hal.inria.fr/inria-00101077
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:55:51
Dernière modification le : mardi 24 avril 2018 - 13:36:37

Identifiants

  • HAL Id : inria-00101077, version 1

Collections

Citation

Francis Alexandre. Preuves par récurrence : stratégies et résultats de décidabilité. [Interne] A02-R-489 || alexandre02c, 2002. 〈inria-00101077〉

Partager

Métriques

Consultations de la notice

44