Quelles étaient les lacunes de la procédure de résolution de Robinson?
Paulson et alii. De LCF à Isabelle / HOL dites:
Résolution pour la logique du premier ordre, complète en principe mais souvent décevante en pratique.
Je pense que complet signifie qu'ils peuvent prouver que n'importe quelle vraie formule dans la logique du premier ordre est correcte. Dans le Manuel du raisonnement automatisé, je trouve:
La résolution est une méthode de démonstration de théorème complète par réfutation: une contradiction (c'est-à-dire la clause vide) peut être déduite de tout ensemble de clauses insatisfaisables.
De Wikipedia:
Tenter de prouver qu'une formule satisfaisable du premier ordre n'est pas satisfaisable peut aboutir à un calcul non final
Pourquoi est-ce décevant?
Réponses
Alors que « décevant dans la pratique » est certainement pas définissable formellement, contrairement à « complet » ( ce qui ne fait dire « peut éventuellement se révéler chaque vraie formule »), il est assez facile de trouver des exemples où naïve résolution n'est pas même à distance suffisante, à savoir des exemples qui devraient être facile à prouver mais quelle résolution est extrêmement lente.
Un exemple célèbre est un codage du principe du casier pour$n$ trous dans la logique propositionnelle (qui est l'énoncé "$n+1$ les pigeons ne peuvent pas s'intégrer $n$trous sans doublons). Il n'y a aucune preuve de cette affirmation en utilisant uniquement une résolution en temps sous-exponentielle$n$.
Les choses sont encore pires dans la logique des prédicats, où il est très facile de trouver des déclarations sans aucune preuve de résolution rapide.
Notez que toute implémentation de résolution doit implémenter une stratégie de sélection des résolvants, ce qui est déjà un problème très difficile, et un domaine de recherche actif, puisque la plupart des algorithmes pratiques pour la démonstration de théorèmes sont des améliorations de la résolution naïve, par exemple l' hyper-résolution .