Abstract FR:

On presente une nouvelle strategie de resolution qui reprend de la methode de wu originale l'utilisation d'un (bon) ordre sur une notion appropriee de chaines de clauses, mais en introduisant une nouvelle notion de chaine et, surtout, une notion de base pour un ensemble de clauses qui tient essentiellement compte de la specificite du cas booleen en eliminant directement les problemes de termes de plus haut degre qui, dans le cas de la methode de wu comme dans sa traduction aux clauses, peuvent necessiter le recours a une iteration couteuse. Ceci revient dans le cas present a gerer de facon soigneuse les tautologies qui peuvent apparaitre dans le processus et a les eliminer autant que possible. Au total, on obtient une methode dont la complexite dans le pire cas est exponentielle