Automatisation de l'application de l'hypothèse de récurrence dans la preuve des formules implicatives
Résumé
L'objectif général de ce travail est de prouver les propriétés des programmes logiques (ensemble de clauses de Horn). Ces propriétés sont des formules de la forme A <-- B où A et B sont des conjonctions d'atomes. Nous disposons d'un ensemble de règles de déductions tels que le pliage, le dépliage et la simplification. La preuve consiste à appliquer l'une de ces règles sur la formule à prouver jusqu'à aboutir à un ensemble de formules triviales. Une étape essentielle dans le processus de la preuve est la réussite du pliage qui peut être vue comme l'application d'une hypothèse de récurrence dans une preuve inductive. Nous proposons des stratégies pour automatiser partiellement le processus de preuve en nous basant sur une analyse statique des formules et des programmes.