Abstract FR:

A partir d'une strategie de controle basee sur les ordres de simplification de termes, il est presente un algorithme de recherche automatique de preuve pour le calcul de sequents, dans le cadre de la logique classique sans egalite. Le calcul de sequents a ete choisi parce que la procedure de preuve pour ce formalisme a le grand avantage de refleter dans la structure meme de l'arbre d'inference la semantique donne a cet arbre. L'algorithme de recherche de preuve presente est prouve correct et complet. Grace a la completude de l'algorithme, il est possible de construire des contre-modeles partiels pour la formule a prouver, si elle n'est pas valide, a partir des sequents de l'arbre d'inference arrete par le controle. Les contre-modeles sont construits sous forme d'inequations pour les termes du langage. Avec la technique de l'evaluation partielle guidee par l'entree, on montre comment construire des propositions de corrections a une formule, a partir des contre-modeles construits, lorsque celle-ci n'est pas consequence logique d'une theorie supposee correcte. Cette technique etend a la logique du premier ordre la technique d'apprentissage a partir d'explications des echecs, proposee dans le cadre des clauses de horn. L'algorithme de recherche automatique de preuve presente a des applications en programmation logique, ou il l'approche plus de son ideal, grace a une plus grande declarativite et un plus grand pouvoir d'expression. Il peut automatiser l'oracle dans les algorithmes de detection d'erreurs de programmes prolog. La technique de construction de corrections, dans ce cadre, permet de proposer des candidats a la correction des erreurs detectees. Il sert aussi a une application de l'apprentissage symbolique au paradigme de la generation et test en programmation