Quelles étaient les lacunes de la procédure de résolution de Robinson?

Question

paulson et alii. de LCF à Isabelle / Hol Dites:

Résolution pour la logique de premier ordre, complète en principe mais souvent décevante dans la pratique.

Je pense que complète signifie qu'ils peuvent prouver toute formule vraie dans la logique de premier ordre correct.Dans le manuel du raisonnement automatisé je trouve:

La résolution est une méthode de prouve théorème complète réfutionnellement: une contradiction (c'est-à-dire la clause vide) peut être déduite de tout ensemble insatisfait de clauses.

de Wikipedia:

Tentative de prouver une formule satisfaisante de premier ordre comme insatisfaite peut entraîner un calcul non déterminant

Pourquoi est-ce décevant?

Answer 1

tandis que "décevant dans la pratique" n'est certainement pas définitivement formellement, contrairement à "Terminer" (qui signifie effectivement "peut éventuellement prouver toutes les formules vraies"), il est assez facile de trouver des exemples où la résolution naïf n'est même pas à distance adéquat, c'est-à-dire des exemples qui devraient être faciles à prouver, mais quelle résolution est extrêmement lente.

Un exemple célèbre est un codage du Principe du trou de pigeon pour $ n $ trous dans la logique propositionnelle (qui est la déclaration " $ n + 1 $ Les pigeons ne peuvent pas correspondre à $ N $ trous sans doublons). Il n'y a aucune preuve de cette déclaration en utilisant uniquement la résolution dans le temps sous-exponentielle dans $ n $ .

Les choses sont encore pires dans la logique de prédicat, où il est très facile de trouver des déclarations sans preuves de résolution rapide.

Notez que toute mise en œuvre de la résolution doit mettre en œuvre une stratégie de sélection des résolvants, qui est déjà un problème très difficile et une zone de recherche active, puisque la plupart des algorithmes pratiques pour la preuve des théorèmes sont améliorations de résolution naïve, par exemple Hyper-Résolution .