Abstract FR:

Cette these presente de nouvelles fondations pour la programmation en logique disjonctive. La programmation en logique disjonctive etend la programmation en logique pour des clauses de horn par l'introduction de plusieurs atomes dans une tete de clause. Cette extension permet la description d'informations incompletes ou indefinies. Notre approche est basee sur l'etude par cas. Dans un premier temps, nous decrivons dans le cadre de la theorie des preuves le systeme d'inference slou prolog adapte a la programmation en logique disjonctive. Puis dans un deuxieme temps, nous definissons la resolution ou comme extension de la resolution de robinson a l'etude par cas. Nous proposons alors la resolution slou, resultat du mariage du systeme slou prolog et de la resolution ou. La resolution slou sur des programmes de clauses de horn est exactement la resolution sld, base theorique du langage prolog. La programmation en logique calcule les instances des variables d'une question pour qu'elle soit une consequence logique d'un programme. Nous montrons comment la resolution slou permet de calculer de telles instances. L'utilisation de l'etude par cas en resolution slou introduit un fort indeterminisme que nous reduisons grace a l'introduction d'une strategie de parcours de l'espace des preuves dirigee par le but. Enfin, nous comparons la resolution slou avec les membres de la famille des procedures a ancetres