Aufgabe 9.2 d

[Stakkatto]

Hallo,
eine Frage zur Aufgabe 9.2d:
Gehe ich richtig in der Annahme, dass bei Datalog die Auswertung von reachable(g,e) terminieren würde, weil die Reihenfolge der Bedingungen der Regel egal ist? (siehe Datalog Folie 40)

[eneldo]

Hallo,

ja genau, alle Auswertungen würden terminieren, die Reihenfolge spielt keine Rolle, EPP würde terminieren. Datalog ist keine prozedurale Sprache.

Gruß
Eneldo Loza

[Stakkatto]

Okay, vielen Dank!
Liebe Grüße

[barracuda317]

Hallo,

ja genau, alle Auswertungen würden terminieren, die Reihenfolge spielt keine Rolle, EPP würde terminieren. Datalog ist keine prozedurale Sprache.

Gruß
Eneldo Loza

Wo finde ich denn Informationen darüber, wie Datalog einen solchen Beweis führen würde? Würde Datalog eine Fixpunktberechnung durchführen und dann schauen, ob das zu beweisende Faktum enthalten ist? Oder würde Datalog irgendwie erkennen, was für den Beweis relevant ist. Aus den Folien ist mir das leider nicht so ganz klar geworden.

[eneldo]

Wie eine konkrete Implementierung das macht bleibt im Grunde ihr überlassen. Wir können aber einfach davon ausgehen, daß der Datalog-Interpreter eine Fixpunktberechnung durchführt und dann nachschaut, ob ein zu beweisendes Faktum enthalten ist.

[barracuda317]

Wie eine konkrete Implementierung das macht bleibt im Grunde ihr überlassen. Wir können aber einfach davon ausgehen, daß der Datalog-Interpreter eine Fixpunktberechnung durchführt und dann nachschaut, ob ein zu beweisendes Faktum enthalten ist.

Danke, dann ist es mir soweit klar.