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

Résumé en langue originale

L'etude des structures minimales de programmes dans les langages de programmation permet de degager des proprietes interessantes pour l'etude de programmes de tailles plus importantes et de mettre en valeur la puissance d'expression du langage. En programmation logique, le plus petit schema non trivial est constitue d'une clause de horn binaire recursive, d'un fait et d'un but. Des problemes pertinents a etudier concernant ces programmes sont dans un premier temps la terminaison et la satisfiabilite (l'existence de solutions). A l'aide d'une codification inedite de travaux du mathematicien j. H. Conway, nous montrons que ces deux problemes sont indecidables dans le cas general. Des cas particuliers dependant de la (non-) linearite sont egalement etudies. Le resultat sur la satisfiabilite permet de resoudre un probleme ouvert en logique du premier ordre: la satisfiabilite des formules a quatre sous-formules. Une fois ces resultats trouves, il semble logique de se pencher sur la puissance calculatoire de cette classe de programmes. Nous montrons qu'elle est equivalente a celle de machines de turing puisqu'il est possible de construire un meta-interpreteur a clauses de horn qui satisfasse ce schema. Ce resultat peut etre vu comme l'equivalent pour la programmation logique du theoreme de bohm-jacopini pour la programmation imperative.