Ja, herzlich willkommen. Wir hatten letztes Mal kennengelernt, den Resolutionsalgorithmus

erweitert auf Logik erster Stufe. Wir hatten schon festgehalten, wir können von diesem

Algorithmus nicht dasselbe erwarten, wie das, was er für die Aussagenlogik

erleistet. Er ist also kein Entscheidungsverfahren in dem Sinne, dass er

sowohl für erfüllbare als auch für nicht erfüllbare Formeln terminiert und

dann jeweils die richtige Antwort liefert. Was wir aber in der Tat von ihm

bekommen, ist ein Halbentscheidungsverfahren. Das heißt, er

terminiert zumindest dann, wenn die Formel nicht erfüllbar ist. Wenn die

Formel erfüllbar ist, dann kann es mal passieren, dass er terminiert. In

Ausnahmefällen, in Regelfall wird er nicht terminiert.

Dann kann sich streiten natürlich, wie nützlich so ein Algorithmus ist, denn selbst wenn die

Formel nicht erfüllbar ist, wissen wir natürlich nicht, wann der Algorithmus

terminiert. Das heißt, wir stehen da, der kommt nicht wieder und wir wissen es halt

nicht. Sagt er irgendwann noch nicht erfüllbar oder läuft er für immer

weiter. Aber gut, so ist es halt mit Entscheidungsverfahren und wir wissen,

dass nichts besseres geht. Wir wissen es noch nicht, aber man kann zeigen, dass

das Gültigkeitsproblem oder dual das Erfüllbarkeitsproblem in Logik erster

Stufe eben unentscheidbar ist. In anderen Worten, ein Algorithmus, der auf

beiden Fällen terminiert und immer das Richtige antwortet, gibt es nicht.

Wir werden also heute uns damit beschäftigen, diese Vollständigkeit, so

heißt das, das Resolutionsalgorithmus zu beweisen und dazu werden wir als

erstes auch einen Abschnitt der Modelltheorie der First Order Logik noch

abhandeln und zwar die sogenannte Abrauntheorie, also die Theorie der

Abraumodelle.

Ja, Abraumodelle sind also sehr spezielle Modelle, die im Wesentlichen aus

syntaktischem Material bestehen. Das halten wir gleich mal fest.

Die Grundmenge so eines Modells, also die Menge der Individuen, die haben wir ja

mit verschiedenen Zeichnungen belegt oder nicht wir selbst, das ist also Bereich,

Grundbereich oder eben Universum und die Abraumodelle, die haben eben einen pro

Signatur zumindest fest verdrahteten Grundbereich, das sogenannte Abraunt-Universum.

Dafür führen wir Standardnotation ein, u σ, also u wie Universum und den

Index σ, um anzudeuten, dass es eben von der geltenden Signatur σ abhängt und

zwar

ist das eine Menge von Sigma-Termen und zwar die Menge derjenigen Sigma-Termen,

die keine Variablen enthalten. Das heißt, ja gut, irgendwie muss ich meine

Terme natürlich bauen, das heißt also überall da, wo man normalerweise gerne

eine Variable schreiben würde, muss also eine Konstante stehen. Ich füre noch so ein

bisschen Notation ein, also Einsparung von Notationen, wenn wir so einen Term haben,

ja das Universum besteht ja nur aus Termen und den auswerten wollen,

dann heißt das ja, dass wir einen Term auswerten, gegeben irgendein Modell, der von

keinerlei Variablen abhängt, denn er erwähnt ja keine Variable. Wir schreiben

in dem Falle einfach m von Semantikklammern e und das soll stehen eben

für Auswertung von e in irgendeiner Umgebung eta, die aber nicht interessiert,

weil eben die Werte der Variablen für e egal sind. Das heißt, mit anderen Worten in der

Notation sparen wir diese Umgebung für geschlossene Terme ein. Machen wir mal ein

Beispiel dafür, wie also solche Erbran Universum aussehen kann,

indem wir eine konkrete Signatur mal hier nehmen.

Nehmen wir mal folgende Signatur her, die besteht also aus einer einstelligen Funktion

s, einer Nullstelligen Funktion 0, Nullstellig heißt es ist eine Konstante, nimmt keine Argumente

und einem einständigen Prädikat odd, wie ungerade. Das ist also eine Signatur, in der will