Modus ponens ist unvollständig
Betrachten wir folgendes Prolog-Beispiel
%Fakten
cool(peter).
%Regeln
cool(norman) :- cool(dmitri).
cool(dmitri) :- cool(freddy).
cool(freddy) :- cool(mark).
cool(mark) :- cool(patrice).
cool(patrice) :- cool(peter).
|
so ist es leicht einzusehen, dass durch mehrmaliges Anwenden des "Modus ponens" die
Anfrage an das System, ob Norman cool ist, leicht mit
Yes zu beantworten ist.
Man könnte versucht sein, die Schlussregel "Modus ponens" als ausreichend für maschinelles
Schließen zu sehen, was folgendes Gegenbeispiel widerlegt:
Aus der Formeln A→B und ¬B folgt ¬A, was mit dem
Modus ponens nicht ableitbar ist.
Was macht Prolog mit diesem Beispiel?
%Fakten
not(cool(peter)).
%Regeln
cool(norman) :- cool(peter).
|
Obiges Programm erzeugt beim Konsultieren folgende Fehlermeldung:
No permission to modify static_procedure `not/1'
|
Anscheinend darf
not() nicht in dieser Weise verwendet werden. Um auszudrücken,
dass 'Peter nicht cool ist', muss die Aussage 'Peter ist cool' weggelassen werden.
Prolog geht von der
closed world assumption aus, dh. das gesamte Wissen über die
zu untersuchende Welt ist in der Wissensbasis vereint. Und wenn da nicht 'cool(peter)' steht,
dann gilt es eben nicht, dh. das Gegenteil ist richtig. Das modifizierte Programm
%Fakten
%Regeln
cool(norman) :- cool(peter).
|
liefert dann auch richtig:
Schaut man genauer hin, so stellt man fest, dass Prolog nur spezielle Klauseln für Fakten,
Regeln und Anfragen zulässt. Diese Klauseln heißen
Horn-Klauseln. Durch diese
Einschränkung kann Prolog mit Hilfe der Schlussregel
SLD-Resolution
(Linear Resolution with Selection for Definite Clauses) Anfragen maschinell beweisen.
Die angeführten Beispiele ließen sich auch mit der Inferenzregel 'Modus ponens' maschinell
beweisen. Es fehlt ein Beispiel, das die SLD-Resolution notwendig macht und ihre Anwendung
illustriert.
