Preuves par récurrence : stratégies et résultats de décidabilité
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.