Repräsentation des Suchraums

Zusammenfassung

In den vorigen Kapiteln, speziell bei den Konzepten zur Verkleinerung des Suchraums in Kapitel 3, haben wir stets die Formelmengen während des Ableitungsvorgang als Mengen verwaltet und diese Mengen als Zustände des Suchraums interpretiert. Die Zustandsveränderung erfolgte dann pro Ableitungsschritt oder pro Ableitungslevel durch Erweiterung der Formelmenge im vorhergehenden Zustand um die neue(n) Resolvente(n) und ggf. Verminderung um - in ausführlich im 3. Kapitel diskutiertem Sinne - überflüssige Formeln: die neue Formelmenge als neuer Zustand. Daß es andere Möglichkeiten gibt, sowohl Formeln als auch den Suchraum zu repräsentieren, wollen wir in diesem Kapitel darstellen. Dazu werden wir die Grundideen dreier wichtiger Theorembeweiser-Verfahren vorstellen:

Kowalski’s Connection-Graph-Resolution ist eine direkt auf dem Resolutionskalkül basierende Methode und benutzt als zugrundeliegende Datenstruktur einen Graphen, in dem komplementäre Literalpaare der Formelmenge miteinander verbunden werden. Durch Resolution entlang dieser Kanten und bestimmte Vereinfachungsregeln wird dann der Graph manipuliert.