Stratégies de preuves par récurrence basées sur le pliage et le dépliage

Francis Alexandre 1 Moussa Demba 2 Khaled Bsaïes 2
1 DEDALE - Development of specifications
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Résumé : Nous présentons des stratégies de preuves de formules implicatives. Etant donné un programme (ensemble de clauses de Horn), l'objectif général est de démontrer qu'une formule implicative est vraie dans le plus petit modèle de Herbrand de ce programme. Pour résoudre ce problème, on fait appel à des preuves par récurrence. On peut schématiquement distinguer deux approches dans le domaine des preuves automatiques par récurrence: la récurrence explicite qui utilise des règles d'induction et l'induction sans induction qui utilise des procédures de complétion. l'approche décrite ici, basée sur le pliage et le dépliage, peut être classée dans la seconde catégorie. Nous définissons des stratégies et nous les illustrons par des exemples.
Type de document :
Rapport
[Interne] A01-R-284 || alexandre01b, 2001, 14 p
Liste complète des métadonnées

https://hal.inria.fr/inria-00100700
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 14:49:48
Dernière modification le : mardi 24 avril 2018 - 13:32:45

Identifiants

  • HAL Id : inria-00100700, version 1

Collections

Citation

Francis Alexandre, Moussa Demba, Khaled Bsaïes. Stratégies de preuves par récurrence basées sur le pliage et le dépliage. [Interne] A01-R-284 || alexandre01b, 2001, 14 p. 〈inria-00100700〉

Partager

Métriques

Consultations de la notice

91