PROLOG ist eine Programmiersprache, die auf der Hornklausellogik
basiert. In
erster Näherung kann man PROLOG als ein Beweissystem für diese
Teillogik ansehen. Während jedoch ein Hornklauselbeweiser aus der Welt
die Aussage
nicht ableiten könnte, ist PROLOG hierzu
in der Lage. Der über die Technik eines Hornklauselbeweisers hinausgehende
Mechanismus, der PROLOG hierzu befähigt, basiert auf der in
Abschnitt 3.3 behandelten Prädikatsvervollständigung. Sie
ermöglicht eine (nichtklassische) Form der Negation, nämlich die
Negation als Mißerfolg [Cla78].
Die folgende PROLOG-Klausel zur Berechnung eines Elementes der Differenzmenge zweier Mengen illustriert diese Form der Negation in PROLOG.
elem_diff(M,N,X) :- member(X,M), not member(X,N).
not(X) :- call(X), !, fail. |
not(X). |
wie wir sie zuerst in Abschnitt 3.1 im Zusammenhang mit der Annahme der
Weltabgeschlossenheit
eingeführt haben (wobei wie dort die Ableitbarkeit auf der
Objektebene bezeichnet).
Wie die Prädikatsvervollständigung ist die Negation-als-Mißerfolg ein nichtmonotoner Mechanismus, was wir anhand unseres Beispiels 3.2 illustrieren.
kind(larissa). liebt-eiscreme(X) :- kind(X), not abnormal(x). ?- liebt-eiscreme(larissa). yes.Die Anfrage führt zur Instantiierung der Regel des Programms. Deren zweites Unterziel löst den Negationsmechanismus, also einen Aufruf von abnormal(larissa) aus. Da das Programm diese Anfrage nicht lösen kann, verläuft der Aufruf also erfolgreich, so daß das Hauptprogramm mit yes terminiert. Würde man jetzt zusätzlich das Faktum abnormal(larissa) mit in das Programm aufnehmen, so ergäbe sich no als Antwort.
Damit leistet PROLOG offenbar in diesem Beispiel genau das gewünschte Verhalten. Von manchen Autoren wird daher argumentiert, daß diese Programmiersprache für die Zwecke der Formalisierung des alltäglichen Schließens voll ausreicht [Kow91]. Obwohl diese Programmiersprache von großer Ausdruckskraft und deduktiver Stärke ist, bezweifeln die Autoren, daß all die anderen in diesem Buch besprochenen Inferenzformalismen dadurch obsolet werden.
In [Cla78, Llo84] wird die Korrektheit der Negation-als-Mißerfolg
relativ zur Prädikatsvervollständigung gezeigt. Da diese jedoch zu
Inkonsistenzen Anlaß geben kann, wie wir im letzten Abschnitt gesehen
haben, ist die Korrektheit nur für die in Abschnitt 3.3 behandelten
solitären Klauselmengen gesichert. Für diese findet man in den eben
angegebenen Quellen, wo sie als hierarchische
Programme eingeführt
werden, auch einen Vollständigkeitssatz, nach dem dieses Verfahren jede
Antwort auf eine zulässige Anfrage finden kann. In Abschnitt 3.10.3
werden wir eine Semantik dieser hier besprochenen Negation kurz behandeln. Sie
ist eng verwandt mit der in [vRS91] angegebenen Semantik. Technisch
gesprochen besteht das Problem einer semantischen Behandlung der
Negation-als-Mißerfolg in einer Bewältigung der durch Zyklen (siehe
Abschnitt 4.4.4 in [Bib92]), wie zB. , verursachten
Problematik.
Christoph Quix, Thomas List, René Soiron