TypiCal

Au cours de cet exposé, j'expliquerai l'architecture générale des prouveurs basés sur la résolution. Je rappellerai certaines techniques utilisées pour réduire le non-déterminisme lié à l'application de la règle de résolution. En particulier je présenterai la résolution avec ensemble de support et la résolution ordonnée avec sélection, en insistant sur les conditions qui permettent de conserver la complétude réfutationnelle. Nous verrons qu'en combinant ces deux dernières techniques, on peut perdre la complétude réfutationnelle. Je rappellerai alors l'équivalence de cette combinaison avec la résolution modulo polarisé, puis je montrerai que sa complétude est équivalente avec l'admissibilité des coupures en déduction modulo. Je présenterai enfin comment appliquer ces idées pour modifier un prouveur existant (en l'occurrence iprover) afin d'y ajouter la résolution polarisée modulo.