Abstract FR:

Analyse statique du plus simple des programmes récursifs, composé d'un fait "p(a)", d'une règle récursive "p(g) - p(d)" et d'un but "p(t)". Sa modélisation est basée sur un nouvel objet syntaxique, le graphe orienté pondéré. Dans le cadre des systèmes de réécriture en tête, la terminaison d'une règle de réécriture en tête pour tout terme clos est démontrée décidable. Dans le cadre de la programmation logique, pour le plus simple programme récursif contenant un fait et un but linéaires et une règle récursive, il est démontré la décidabilité de l'existence de solutions et de l'arrêt du programme. Les résultats permettent, pour une plus large classe de programmes récursifs, de vérifier facilement leur terminaison, de les compléter et d'améliorer la stratégie de résolution PROLOG dans ces appels récursifs