Abstract FR:

Cette these s'inscrit dans le domaine de la consistance et de l'inference en logique propositionnelle. Apres une presentation generale (partie i), la seconde partie est consacree a la resolution-arriere qui est une nouvelle methode dediee au test de consistance. Elle fait cooperer deux methodes de preuve classiques: l'enumeration et le principe de resolution. Notre methode conduit a prouver l'inconsistance par l'exploration d'un graphe de resolution regulier. Le choix des resolutions a effectuer est guide par l'enumeration, et les resolutions binaires effectuees pendant les retours-arriere permettent de couper des sous-arbres inutiles dans la preuve. De plus, toutes les resolvantes binaires ne sont pas memorisees, ce qui correspond au concept usuel de clash. Nous presentons ensuite un pretraitement base sur la recherche locale, dont le but est d'ameliorer l'heuristique de choix du litteral de branchement. La troisieme partie traite de la deduction. Les concepts de p-impliquant et p-implique m-premiers, extension de la notion de champ de production , sont introduits. Nous proposons un algorithme qui calcule les p-impliquants et les p-impliques m-premiers de formules sous forme normale conjonctive ou disjonctive en une ou deux passes. Cet algorithme est enumeratif et a la particularite d'eviter l'operation explicite de suppression des sous-sommations, effectuee habituellement. En outre nous montrons comment, lorsque deux passes sont necessaires, l'introduction de nouvelles variables permet de reduire la taille de la premiere passe. La quatrieme partie regroupe un ensemble de cas d'instances pour le probleme de la consistance. Nous presentons un generateur d'instances aleatoires consistantes qui permet de mettre en avant les faiblesses des algorithmes de recherche locale. La derniere partie est consacree aux tests illustrant les algorithmes implementes