Was waren die Mängel von Robinsons Abwicklungsverfahren?
Paulson et alii. Von LCF zu Isabelle / HOL sagen Sie:
Auflösung für Logik erster Ordnung, im Prinzip vollständig, in der Praxis jedoch häufig enttäuschend.
Ich denke, vollständig bedeutet, dass sie jede wahre Formel in der Logik erster Ordnung korrekt beweisen können. Im Handbuch des automatisierten Denkens finde ich:
Die Auflösung ist eine widerlegungsvollständige Theorembeweismethode: Ein Widerspruch (dh die leere Klausel) kann aus jedem unbefriedigenden Satz von Klauseln abgeleitet werden.
Aus Wikipedia:
Der Versuch, eine erfüllbare Formel erster Ordnung als nicht erfüllbar zu beweisen, kann zu einer nicht abschließenden Berechnung führen
Warum ist das enttäuschend?
Antworten
Während "enttäuschend in der Praxis" formal sicherlich nicht definierbar ist, im Gegensatz zu "vollständig" (was in der Tat bedeutet, "kann schließlich jede wahre Formel beweisen"), ist es ziemlich einfach, Beispiele zu finden, bei denen eine naive Auflösung nicht einmal annähernd angemessen ist, dh Beispiele, die dies sollten leicht zu beweisen sein, aber welche Auflösung extrem langsam ist.
Ein berühmtes Beispiel ist eine Kodierung des Taubenlochprinzips für$n$ Löcher in der Aussagenlogik (das ist die Aussage "$n+1$ Tauben passen nicht hinein $n$Löcher ohne Duplikate). Es gibt keinen Beweis für diese Aussage, wenn nur die Auflösung in der Zeit subexponentiell in verwendet wird$n$.
Noch schlimmer ist es in der Prädikatenlogik, wo es sehr einfach ist, Aussagen ohne schnelle Auflösungsbeweise zu finden.
Beachten Sie, dass jede Implementierung der Auflösung eine Strategie zur Auswahl der Lösungsmittel implementieren muss, was bereits ein sehr schwieriges Problem darstellt, und ein aktives Forschungsgebiet, da die meisten praktischen Algorithmen zum Nachweis von Theoremen Verbesserungen der naiven Auflösung sind, z . B. Hyperauflösung .