Up !
Illner Solutions
3. 2. 4 Resolutionskalkül R2
In
diesem Abschnitt geht es um die praktische Anwendung der klassischen
Prädikatenlogik beim automatischen Schließen. Das Resolutionskalkül R2
ist ein Algorithmus, mit dem man die Gültigkeit von komplexeren
Aussagen durch Widerspruchsbeweis zeigt. Es wird dabei versucht, das
Gegenteil zu widerlegen.
Das gelingt wiederum durch ... Aus KNF werden Horn-Klauseln. Dies kann man in PROLOG und in LISP ?
3. 2. 4. 1 Normalisierung von Aussagen
3. 2. 2. 2 Resolution von Klauseln
3. 2. 2. 3 PROLOG
3. 2. 4. 1 Normalisierung von Aussagen
Komplexere
prädikatenlogische Ausdrücke können auf eine ähnliche syntaktische Form
gebracht weren, so dass man mit ihnen Schließen? kann.
Pränexform
...
Skolemform
...
Klauselform
...
3. 2. 4. 2 Resolution von Klauseln
Boolesche
3. 2. 4. 3 PROLOG
Die Klauselform wird nun als Grundlage für die logische Programmiersprache PROLOG (... 19xx).
Man startet ein Programm hier nicht über eine Main()-Funktion, sondern durch eine Start-Query. Man fragt:
- P(a, b) ? - Wenn dieser Fakt als Fakt vorhanden ist oder mit Regeln abgeleitet werden kann, dann liefert das Programm W.
- P(a, x) ? Hier ist x eine Variable und das Programm liefert eine Liste von Fakten P(a, x) mit verschiedenen x.
Erstmals kreiert am – Sonntag, 04. Februar 2018
Letzrmals geändert am – Donnerstag, 09. Januar 2020
Autor: Korgüll
Copyright 2018 – 2020 Illner Solutions