• Langue : Français
• Discipline : Informatique
• Identifiant : Inconnu
• Type de thèse : Doctorat
• Date de soutenance : 01/01/1991

Résumé en langue originale

Les interpréteurs Prolog ne sont pas complets en général pour les échecs et pour les succès car ils sont basés sur un parcours de l'arbre de résolution en profondeur d'abord associé à une gestion des buts en pile. Cependant, la résolution SLD sur laquelle Prolog est basé est correcte et complète. L'utilisation d'une règle d'évaluation équitable tout sous-but qui apparaît dans une dérivation infinie est effectivement sélectionné permet d'obtenir tous les échecs finis et tous les succès finis d'un programme: s'il existe un arbre de dérivation SLD fini pour un programme P et un but B, alors tout arbre de dérivation équitable pour P et B est fini. Un interpréteur Prolog équitable permet donc d'éviter toutes les boucles liées à l'ordre d'évaluation des sous-buts. Nous étudions l'utilisation de règles d'évaluation équitables en Prolog, des aspects théoriques aux aspects pratiques. Deux modèles de règles d'évaluation équitables, Pile-indicée et Arbres-de-buts-indicés sont proposés. Ces stratégies de dérivation sont basées sur l'utilisation d'indices de dérivation pour contrôler l'ordre d'évaluation des sous-buts. Des implémentations efficaces de ces règles ont été réalisées. Les problèmes pratiques liés à l'utilisation d'un ordre d'évaluation différent sont pris en compte et nos interpréteurs équitables sont effectivement utilisables