Retour à la page du séminaire

16/03/2000 : Gilles Dowek (Inria)
A quoi sert l'élimination des coupures en démonstration automatique ?

résumé

Il est bien connu que la logique d'ordre supérieur peut être exprimée comme une théorie du premier ordre. En démonstration automatique, cela signifie qu'on peut utiliser la résolution du premier ordre pour rechercher des démonstrations en logique d'ordre supérieur. La méthode ainsi obtenue a une preuve de complétude beaucoup plus simple que celle la résolution d'ordre supérieur (qui repose sur le théorème d'élimination des coupures d'ordre supérieur) mais elle est beaucoup plus inefficace. On propose une restriction de cette méthode qui simule pas à pas la résolution d'ordre supérieur. Cette restriction est complète mais sa démonstration de complétude demande d'utiliser un résultat logiquement aussi fort que le théorème d'élimination des coupures d'ordre supérieur. Ce théorème de complétude est de plus indépendante de la logique d'ordre supérieur.