Aufgabe 9.2 d

Stakkatto
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 19. Okt 2011 15:50

Aufgabe 9.2 d

Beitrag von 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
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 220
Registriert: 19. Mai 2006 13:06
Kontaktdaten:

Re: Aufgabe 9.2 d

Beitrag von 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
Windoof-User
Windoof-User
Beiträge: 24
Registriert: 19. Okt 2011 15:50

Re: Aufgabe 9.2 d

Beitrag von Stakkatto »

Okay, vielen Dank!
Liebe Grüße

barracuda317
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Re: Aufgabe 9.2 d

Beitrag von barracuda317 »

eneldo hat geschrieben: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
Sonntagsinformatiker
Sonntagsinformatiker
Beiträge: 220
Registriert: 19. Mai 2006 13:06
Kontaktdaten:

Re: Aufgabe 9.2 d

Beitrag von 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
Endlosschleifenbastler
Endlosschleifenbastler
Beiträge: 187
Registriert: 12. Okt 2011 18:15

Re: Aufgabe 9.2 d

Beitrag von barracuda317 »

eneldo hat geschrieben: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.

Antworten

Zurück zu „Archiv“