Herzlich willkommen und ein Frohes neues Jahr.

Ja, wir befassen uns heute mit algorithmischen Aspekten der Logik erster Stufe.

Anders als die Aussagenlogik ist die逻 motionsusting die Logik erster Stufe leider, oder zum Glück je nachdem wie man's sehen will, nicht entscheidbar.

Also ich kann nicht einen Algorithmus bauen, der mir

für jede Formel in Prädikatenlogik erster Stufe sagt,

ob sie nun zum Beispiel gültig ist oder nicht.

Das hier zu beweisen führt uns zu weit, aber

wir können uns der Sache zumindest von unten her annähern 화장.

Na, ja, also die Tatsache ist, dass ein Problem

unentscheidbar ist, hat die Informatik noch nie von was abgehalten.

Es gibt reinweise erfolgreiche automatische Beweiser für Logik eigentlich.

Gut, da merkt man dann halt, dass die nicht jede Formel, die man Ihnen vorwürft, einfach

so mal eben bewiesen kriegen.

Können sie halt auch nicht.

Trotzdem gibt es eben etablierte Algorithmen.

Und wir werden einen heute kennen lernen und wir werden später auch von diesem Algorithmus

zeigen, dass er vollständig ist, mit anderen Worten, dass er jede Formel bewiesen kriegt,

so sie denn wahr ist.

d.h. gültig ist. Das Dumme ist, wenn die Formel nicht hilltig ist,

dann kommt die Prozedur womöglich nicht zurück.

Wir wissen ja vorab womöglich nicht, ob sie gültig ist.

S.h. warten alleine hilft aber nicht.

Und wir wissen ja nicht, ob er noch einfach noch nicht

fertig ist mit Beweisen. Oder ob er womöglich nie fertig wird,

weil die Formel eben nicht beweistbar ist.

Das surveillance service

Gut, aber so ist das Leben. Wir brauchen dafür etliches an Vorbereitung.

Die Vorbereitung ist ähnlich, wie bei unserem Algorithmus für Aussagenlogik

– in erster Linie – eine Sache von Normalisierungen.

Also wir nehmen uns eine Formel und normalisieren die in ein Format,

dass oder art für den Algorithmus geeignet ist.

Der Algorithmus ist dann der selbe wie für Aussagenlogik.

Am Ende ist es also ein Resolutionsalgorithmus.

Gut, es gibt anderthalb Feinheiten, die man auch zusätzlich beachten muss, unter anderem

eben diese Unifikation, die wir letztes Mal kennengelernt haben.

Aber der grundsätzliche Algorithmus ist erst einmal derselbe.

Wir beginnen jetzt mit dieser Frage der Normalfur.

Ich werde jetzt einmal diese langwierige Logikerstufe oder Prädikaten Logikerstufe

nur nicht mehr an die Tafel schreiben.

Ich werde es meist noch sagen, aber wenn ich es okayíre, werde ich es nur kurz schreiben und

das auf writerisch welches ich ichvised.

Es geht um Normalformen in logikerster Stufe.

Das Wort Normalformen ist mir zu lang

also das kürze ich jetzt ab mit nf.

Und die erste der Normalformen ist die sogenannte Pränexe-Normalform.

So, ich definiere jetzt also ein grammatikalisches Format für bestimmte Formen, die ich dann Pränexe-Normalformen nenne

und zeige anschließend, dass ich jede Formel äquivalent in eine solche Pränexe-Normalform umformen kann.

So, Pränexe-Normalformen sind also bestimmte Formeln in der Sprache, die wir bisher schon kennen.

Und zwar folgender Art.

So, sie hat also diese etwas lustig anmutende Form zunächst mal von der Notation her.