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