Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

So, okay, ich denke jetzt müsste es gehen.

Ich habe noch eine Korrektur nachzuliefern und zwar bezieht sich diese Korrektur nicht auf den Tafelanschrieb, sondern auf das, was ich zum Tafelanschrieb gesagt habe.

Man kann sich ja jetzt dank der Aufnahme, kann man ja auch die mündlichen Fehler jetzt nachverfolgen und der Fehler, um den es geht, ist folgender.

Wir hatten über etwas gesprochen, das hieß Abran vollständigkeit.

Erbran vollständigkeit heißt, wenn eine Formel oder eine Formelmenge überhaupt erfüllbar ist, hat sie auch nicht nur für Formeln oder Formelmengen, sondern nur für Formeln dieser Form hier,

für den universellen Abschluss von Phi und zwar nicht etwa für beliebige universelle Abschlüsse, also insbesondere, wenn Phi aus geschlossenen Formeln besteht, tut der universelle Abschluss ja gar nichts.

Das wäre also Quatsch.

Haben wir auch nicht so formuliert, also der Satz war mit korrekten Voraussetzungen bewiesen.

Er wird auch mit richtigen Voraussetzungen im Prinzip angewendet. Das hier gilt nur für Phi-Quantoren frei.

Wir hatten ihn verwendet für den Fall, dass Phi ein definiertes Programm ist.

Definierte Programme sind insbesondere von dieser Form für alle Phi- und Phi-Quantoren frei.

Das heißt also, die an der Stelle war auch korrekt verwendet.

Der Satz nur, das was ich zum Tafelanschrieb da gesagt habe, war in dem Moment falsch. So, Korrektur.

Ja, wir waren dabei uns anzusehen SLD-Resolution. Wir hatten sie definiert.

SLD-Resolution besteht also in Anwendung der offensichtlichen Resolutionsregel.

Also wir verketten einfach Implikationen in der erwarteten Weise mit dem einzigen zusätzlichen Twist, das wir eben unifizieren müssen.

Das heißt, wenn zum Beispiel ein Unterziel, das wir gerade beweisen wollen und der Kopf einer Regel, die wir anwenden wollen, nicht wörtlich übereinstimmen,

dann müssen wir eben durch Unifikation dafür sorgen, dass sie es doch tun.

Und haben dann das Unterziel auf ein entsprechend spezialisiertes reduziert.

Der Gag an SLD-Resolution war jetzt der, dass wir eine Stufe Nicht-Determinismus aus diesem Verfahren rausnehmen.

Was für Nicht-Determinismus gab es? Drei Quellen wesentlich? Ja?

Was, die sind alle? Das kann ich nicht sagen. Der wollte gerade sagen, das waren irgendwie 80 Tanz. Das kann ich nicht sagen.

Jeder nur ein Kreuz. Mehrfach teilnehmen gilt als schummeln.

Also was sind die Quellen von Nicht-Determinismus in diesem Verfahren?

Also erstens, wir müssen uns aussuchen, auf welches Unterziel wir überhaupt uns als erstes konzentrieren.

Zweitens, wir müssen uns aussuchen, welche Regel wir anwenden.

Drittens, wir müssen den Unifikator wählen.

So, zwei von diesen Quellen lassen sich ausschalten.

Das eine ist offensichtlich, statt eines beliebigen Unifikators nehmen wir einfach immer den allgemeinsten.

Damit liegen wir offensichtlich nie falsch.

Zweiter Punkt ist der, wir schalten den Nicht-Determinismus hinsichtlich der Auswahl des Unterziels aus,

die sich eben auch auf eine Selektionsfunktion, eine sogenannte Berechnungsregel zugrunde legen.

Das ist eben das S in SLD Resolution, also S wie Selection Function.

Das Typische eben, die Prologregel, ist die, dass man schlicht und einfach immer das erste der aufgelisteten Unterziele sich vorknüpft.

Die dritte Quelle von Nicht-Determinismus, die werden wir nicht los, nämlich die Auswahl der Regel, die wir anwenden wollen.

Wir werden nachher hoffentlich noch beweisen, dass SLD Resolution vollständig ist.

Das ist deswegen so ein bisschen überraschend, weil es ja zunächst mal doch relativ einschränkend aussieht,

dass man keine Wahl mehr hat, welches Unterziel man als erstes erledigt.

Vorher schauen wir uns nochmal an ein weiteres Beispiel.

Wir formulieren dann auch erst die Korrektheit und dann die Vollständigkeit der SLD Resolution.

Also, noch ein Beispiel.

Also wieder mit der Append Funktion, die wir auch im vorigen Beispiel schon verwendet hatten.

Nehmen wir zum Beispiel an, wir hätten diese Anfrage hier. Append einer Liste 1, X, zusammengesetzte Liste Z, Y.

Wir fragen also nach allen Listen X, die, wenn sie mit 1 zusammengesetzt werden, eine zusammengesetzte Liste Z, Y ergeben.

Darauf gibt es offenkundig unendlich viele Antworten.

Also insbesondere jede Liste X wird da ja vorkommen, denn wenn ich 1 vorne dran hänge, dann ist das, was durch Zusammenhängen von 1 und X entsteht, auf jeden Fall eine zusammengesetzte Liste.

Also ich meine, die Alternative wäre, dass eine leere Liste ist. Das wird natürlich nie vorkommen, wenn ich vorne eine dran hänge, die schon ein Element hat.

Der Witz an diesem Beispiel ist zu illustrieren, dass ich in so einer SLD-Herleitung durchaus Variable überbehalten kann.

So, das Besondere ist, also hierauf, ja, machen wir einfach mal die entsprechende Resolution.