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

Résumé en langue originale

La sémantique opérationnelle des programmes Prolog(définis) la plus fréquemment étudiée fait implicitement l'hypothèse que ces programmes sont évalués par des interpréteurs idéaux (en largeur d'abord et équitables). En conséquence, les résultats théoriques très complets qui ont été obtenus jusqu'à présent ne s'appliquent pas aux interpréteurs standard usuels. Nous définissons de nouvelles sémantiques opérationnelles, adaptées aux interpréteurs standards ou plus généralement, décrivant un noyau calculable quel que soit l'interpréteur envisagé. Nous montrons ensuite que ces sémantiques peuvent être caractérisées axiomatiquement ; ces résultats constituent donc une version plus réaliste et plus générale des résultats classiques. Nous avons utilisé, au cours de cette étude, une technique de dédoublement des symboles de prédicats dont nous avons étudié systématiquement les rapports avec la logique trivaluée. Nous avons également démontré des théorèmes de complétude en logiques bivaluée et trivaluée s'appliquant à des classes générales de programmes logiques (comprenant bon nombre des traductions axiomatiques rencontrées en programmation logique) dans le cadre de la Théorie Équationnelle de Clark.