Abstract FR:

En utilisant des techniques issues de la démonstration automatique, nous proposons dans cette thèse un mécanisme d'exécution des programmes logiques adapté aux contraintes et à la programmation logique équationnelle. Cette méthode, qui utilise des techniques de simplification, peut être considérée comme un moyen de combiner des stratégies ascendantes et descendantes. Cette approche possède de plus deux atouts majeurs par rapport aux mécanismes usuels: d'une part, nous obtenons une propriété de synthèse de l'ensemble des réponses pour de nombreuses quêtes, d'autre part, l'usage de la règle de simplification permet de réduire l'espace de recherche et donc, dans certains cas, d'éviter des boucles. On peut distinguer trois étapes dans notre travail: programmes logiques avec contraintes: tout d'abord, nous proposons une extension minimale prenant en compte des contraintes non symboliques et permettant de conserver les propriétés de terminaison et de synthèse énoncées plus haut. Traitement de la négation: l'adjonction au système précèdent de certaines règles permet de traiter la négation dans les programmes logiques contraints. Ceci est à rapprocher des travaux sur la négation constructive. Programmes logiques équationnels : notre méthode s'adapte également aux programmes logiques comportant une théorie équationnelle, sans négation, définie par l'utilisateur. Dans un certain nombre de cas, notre approche permet de réduire le nombre de pas d'inférences ascendantes.