thesis
Variantes de l'algorithmes de sl-résolution avec retenue d'informations : démonstration de l'équivalence entre sl-résolution et production et démonstration de la validité de la variante des impasses et de la variante de remontée d'impasses
Institution:
Aix-Marseille 2Disciplines:
Directors:
Abstract EN:
Pas de résumé disponible.
Abstract FR:
En depit des nombreuses strategies ameliorant l'algorithme de sl resolution, beaucoup d'informations redondantes et inutiles etaient generees, notamment lors d'echec d'effacement de litteraux. Un algorithme, appele slri, est propose. Il tient compte de ces informations. Il est demontre que l'arbre de recherche de cet algorithme est inclus dans l'arbre de recherche de la sl resolution