Resolutionskalkül
aus Wikipedia, der freien Enzyklopädie
Der Resolutionskalkül ist ein logischer Kalkül, der insbesondere im Rahmen des automatischen Beweisens, einer Teildisziplin der Künstlichen Intelligenz, zum Einsatz kommt. Er basiert auf der sogenannten Klauselsprache oder auch Klauselform. Bei der Klauselform handelt es sich um eine Mengendarstellung von Ausdrücken, die sich in konjunktiver Normalform befinden. Auf der Basis der Klauselform wird im Resolutionskalkül eine einzige Inferenzregel verwendet.
Wichtige Ziele bei der Bildung von Kalkülen sind Korrektheit und Vollständigkeit. Im Zusammenhang mit automatisierten Beweisverfahren erweist sich die Vollständigkeit jedoch auch als problematisch. Insbesondere werden durch vollständige Kalküle auch alle allgemeingültigen Formeln sowie alle Spezialisierungen herleitbarer Formeln erzeugt. Der Resolutionskalkül gilt als Ausweg für die sich widersprechenden Anforderungen an ein Kalkül beim automatischen Beweisen.
Der Resolutionskalkül unterscheidet sich für Aussagenlogik und Prädikatenlogik. Für die Aussagenlogik liefert der Resolutionskalkül ein Entscheidungsverfahren bzgl. der Erfüllbarkeit der in Frage stehenden Formel, für die Prädikatenlogik lediglich ein Semi-Entscheidungsverfahren. Letzteres äußert sich darin, dass das Verfahren für erfüllbare prädikatenlogische Formeln nicht notwendigerweise anhält.
[Bearbeiten] Bestandteile des Resolutionskalküls
- Literale: Als Literale werden positive oder negierte atomare Formeln betrachtet.
- Klauseln: Eine Klausel ist eine endliche Menge von Literalen, die für die Disjunktion aller enthaltenen Literale steht. Die leere Klausel repräsentiert einen Widerspruch.
- Eine Menge von Klauseln wird als Konjunktion der enthaltenen Klauseln interpretiert.
[Bearbeiten] Der Resolutionskalkül für die Aussagenlogik
Wir formulieren die Resolutionsregel, gelegentlich auch Resolventenregel genannt, in der Mengensprache der Klauselform.
- C1 und C2 seien zwei Klauseln mit den Literalen L1 = A und
. - Dann bezeichnet man die Vereinigungsmenge der beiden Klauseln ohne L1 und L2 als die Resolvente C von C1 und C2, d.h.
.
Die Resolvente ist eine logische Folge von C1 und C2. Um sich dies klar zu machen, muss man sich lediglich die Definition einer logischen Folge vergegenwärtigen (siehe Logik): Eine Formelmenge G folgt logisch aus einer Formelmenge F, wenn jede Interpretation, die F erfüllt, auch G erfüllt. Im konkreten Fall erkennt man leicht, dass jede Interpretation, die sowohl C1 als auch C2 erfüllt, wenigstens eine der Klauseln 
oder 
und damit auch C erfüllen muss, das diese ja nur disjunktiv verknüpft.
[Bearbeiten] Andere Kalküle im logischen Einsatz
- Baumkalkül: in gewisser Weise unter den Kalkülen der nächste Verwandte des Resolutionskalkül
- axiomatische Kalküle
- Systeme natürlichen Schließens
- Sequenzenkalkül
- Existential Graphs
| Dieser Artikel oder Abschnitt ist noch unvollständig und weist folgende Lücken auf: Weitere Ausarbeitung der formalen Aspekte, Geschichtliche Entwicklung mit Autoren- und Quellenangaben, Literatur Hilf Wikipedia, indem du ihn erweiterst und ihn jetzt vervollständigst! |
