Ist die Auflösung vollständig oder nur die Widerlegung vollständig?

Wenn man durch einige Wissensrepräsentation Tutorials auf Auflösung im Moment, und ich kam in Dia 05.KR, no77 .

Dort wird erwähnt, dass "das Verfahren auch abgeschlossen ist".

Ich denke, diese Vollständigkeit kann nicht bedeuten, dass ein Satz, der von KB stammt, durch Auflösung abgeleitet wird. Beispielsweise kann die Auflösung nicht aus einer KB mit einer einzelnen Klausel abgeleitet werden . (Beispiel aus KRR, Brachman und Levesque, Seite 53).$(q \lor \neg q)$$\neg p$

Könnte mir jemand helfen, herauszufinden, was in dieser Folie gemeint ist? Bezieht sich die Vollständigkeit der Folie auf die vollständige Widerlegung und nicht auf ein vollständiges Beweisverfahren?

Die Auflösung ist als Widerlegungssystem vollständig. Das heißt, wenn ein widersprüchlicher Satz von Klauseln ist, kann die Auflösung widerlegen , dh .$S$$S$$S \vdash \bot$

Dies ist ausreichend , da entspricht . Wenn wir also sehen wollen, dass eine Formel von , müssen wir nur prüfen, ob es einen Widerlegungsnachweis für gibt, der mit der Auflösung überprüft werden kann.$T \vdash A$$T \cup \{\lnot A\} \vdash \bot$$A$$T$$T \cup \{\lnot A\}$

Die Auflösung ist, wie Sie erwähnt haben, nur widerlegungsmäßig vollständig. Dies ist beabsichtigt und sehr nützlich, da es den Suchraum drastisch reduziert. Anstatt irgendwann jede mögliche Konsequenz ableiten zu müssen (um einen Beweis für eine Vermutung zu finden), versucht die Lösung nur, die leere Klausel abzuleiten.

Es ist auch implizit vollständig in folgendem Sinne:

Wenn ein Satz von Klauseln eine nicht tautologisch Klausel impliziert , dann ist es immer möglich , eine einzige Klausel abzuleiten die subsumiert (dh ).$F$$C$$C'$$C$$C' \subseteq C$

Quelle:
Christian G. Fermüller, Implizite Vollständigkeit der unterzeichneten Entschließung, 2002

Beachten Sie, dass sich das ursprüngliche Ergebnis auf Folgendes bezieht:
RCT Lee. Ein Vollständigkeitssatz und ein Computerprogramm zur Ermittlung von Theoremen, die aus gegebenen Axiomen abgeleitet werden können. Ph.D. Diplomarbeit, Universität von Kalifornien, Berkely, 1967.