EPP und Negation

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

EPP und Negation

Beitrag von The One and Only Markus »

Hi,

kann mit jemand mal erklären wo das Problem mit der Negation beim EPP besteht? In den Folien steht dass Negation mit einfacher Fixpunktsemantik nicht in den Griff zu bekommen ist. Man kann sich doch einfach den Fixpunkt mit dem EPP berechnen und wenn mein Literal dann nicht dabei ist habe ich doch das Inverse des Literals bewiesen (wegen der closed world assumption).Insbesondere der Satz "Zu keinem Zeitpunkt der iterativen Anwendung von EPP kann man
sicher sagen, daß ein Literal nicht noch später bewiesen wird" ist doch falsch. Wenn ich den Fixpunkt erreicht habe kann man sehr wohl sagen, dass nichts neues mehr bewiesen wird.
Das Problem mit den Zyklen und Negation sehe ich ein, aber darauf wird ja nicht eingegangen, also muss es noch ein anderes Problem geben. Nur welches ist das??

Gruß
Markus

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: EPP und Negation

Beitrag von Steven »

Der Satz "Zu keinem Zeitpunkt der iterativen Anwendung von EPP kann man sicher sagen, daß ein Literal nicht noch später bewiesen wird" ist leider richtig. Die Fixpunktiteration muss keine endliche Folge erzeugen, d.h. du hat mit etwas Pech unendliche viele Iterationen. Möchtest du bspw. "brot(weißbrot)" beweisen, dann machst du so viele Iterationen, bis "brot(weißbrot)" auftaucht, danach kannst du abbrechen. Mit einer Negation ("not(brot(gummiball))") müsstest du aber den nicht existierenden Fixpunkt herleiten, und dann schauen, dass darin nirgends "brot(gummiball)" auftaucht. Das geht nicht. FO (Prädikatenlogik erster Stufe) ist unentscheidbar, die wahren Aussagen sind zwar rekursiv aufzählbar, ihr Komplement aber leider nicht.
Das hat leider ein paar ganz unschöne Konsequenzen, nehmen wir mal folgendes Programm:

Code: Alles auswählen

odd(1).
odd(X) :- X > 2, odd(X-2).
brot(X) :- gebacken(X).
gebacken(weißbrot).
ball(gummiball).
Wir wollen "not(brot(gummiball))" beweisen. Leider produziert die odd-Regel eine unendliche Folge, wenn wir die natürlichen Zahlen als Teil unseres Herbrand-Universums ansehen. Das hat zwar nichts mit unserer Anfrage zu tun, aber da wir keinen Fixpunkt haben, kann Datalog einfach nicht wissen, dass nicht vielleicht nach n Iterationen doch noch "brot(gummiball)" kommt. Schließlich gibt es noch Regeln, die man anwenden kann.

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Re: EPP und Negation

Beitrag von The One and Only Markus »

Ah ok, sowas in der Art hatte ich schon vermutet, aber nicht zu Ende gedacht ^^. Ich dachte erst das widerspricht sich mit der Vollständigkeit des EPP. Aber nur weil man alle wahren Fakten (in endlicher Zeit) herleiten kann, heißt das ja nicht dass man für alle nicht wahren Fakten sagen kann, dass sie nicht herleitbar sind. Danke :)

Steven
Kernelcompilierer
Kernelcompilierer
Beiträge: 425
Registriert: 2. Sep 2008 10:00
Wohnort: Frankfurt am Main

Re: EPP und Negation

Beitrag von Steven »

The One and Only Markus hat geschrieben:... heißt das ja nicht dass man für alle nicht wahren Fakten sagen kann, dass sie nicht herleitbar sind.
Das kann man aber sagen, da EPP konsistent ist :). EPP wird niemals einen zu den Regeln und bereits abgeleiteten Fakten inkonsistente Aussage herleiten.

Überlege es dir anders: Man kann theoretisch eine Maschine konstruieren, die jede Sekunde eine Iteration ausführt und die Ergebnisse ausgibt. Jetzt will ich zeigen, dass eine bestimmte Aussage nicht gilt, also not(A). Ich weiß, dass meine Maschine A bisher noch nicht ausgegeben hat, aber ich weiß nicht, ob sie es noch tut, wenn ich nur lange genug warte. Um not(A) zu zeigen, muss ich aber wissen, dass meine (korrekte) Maschine niemals A ausgeben wird. Das kann ich aber nicht, denn ich weiß nicht, was sie noch alles ausgibt, wenn ich nur lange genug warte - die Maschine läuft ja unendlich lange.
Das Problem ist einfach, dass ich keine komplementäre Maschine konstruieren kann, die alle nicht wahren Aussagen ausgibt - dann müsste ich ja nur beide Maschinen parallel laufen lassen und warten, bis eine der Maschinen A ausgibt. Je nachdem ob es die "wahr-Maschine" oder die "falsch-Maschine" war, wüsste ich dann, ob A oder not(A) gilt. Leider ist eine solche "falsch-Maschine" für FO prinzipiell unmöglich.

The One and Only Markus
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 169
Registriert: 10. Nov 2005 19:28
Wohnort: Darmstadt

Re: EPP und Negation

Beitrag von The One and Only Markus »

Jo sorry, ich hab mich da falsch ausgedrückt. Man sollte immer sparsam mit mehreren Verneinungen in einem Satz umgehen :D. Hab schon verstanden wie das läuft, man muss nur sein FGdI2 Wissen reaktiviern und schon wird das alles klar ^^

Antworten

Zurück zu „Archiv“