Abstract FR:

Ce travail propose un cadre formel general pour l'etude de backtracking intelligent en programmation logique. On expose d'abord un algorithme d'unification etendue permettant de connaitre l'historique des liaisons en associant un graphe a un systeme d'equations. L'unifiabilite de celui-ci se caracterise par des proprietes simples de ce graphe. En particulier, on peut determiner les causes de non-unifiabilite. L'exploitation de cette information est a la base du schema de backtracking intelligent presente ensuite. Celui-ci procede de trois alternatives: ordre partiel ou total sur les nuds de l'arbre de preuve, analyse plus ou moins fine des causes de non-unifiabilite, generation parallele ou sequentielle des points de backtracking. On etablit la completude des calculs intelligents que ce schema definit par rapport aux calculs exhaustifs comparables. On retrouve comme instances particulieres du schema les differentes methodes existantes. On s'interesse alors a l'instance la plus proche de prolog, c'est-a-dire celle qui utilise un ordre total (lexicographique), une analyse sommaire de non-unifiabilite et une generation sequentielle des points de backtracking, la conjonction de ces choix engendrant des simplifications importantes. Finalement, cette methode est encore simplifiee en vue d'une implementation, aux depens de l'intelligence du backtracking cette fois-ci