TypiCal

Depuis le théorème de Gödel, on sait que, dans toute extension cohérente de l'arithmétique, il existe des propositions qui ne sont pas démontrables, mais qui le deviennent dans certaines extensions de cette théorie. On montre, dans cet exposé, que les propositions qui expriment la complétude d'une méthode de démonstration automatique, c'est-à-dire la propriété que cette méthode trouve, en un temps fini, une démonstration pour toutes les propositions démontrables, sont des exemples de telles propositions. La théorie dans laquelle on peut démontrer la complétude d'une méthode de démonstration automatique donne un certain nombre d'informations sur ce que cette méthode peut faire et sur ce qu'elle ne peut pas faire. On illustrera ce point par une comparaison entre la résolution ordonnée avec sélection et la résolution modulo.