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

Wir haben vorweg zwei technische Angelegenheiten.

Erstens war gebeten worden, um die, sagen wir mal, Eruierung der Möglichkeit,

die Intensivübung auf einen anderen Slot zu schieben.

So, Frühsenil. Die Abstimmung war gefallen auf den Donnerstag, nicht wahr?

Irre ich mich? Ja. Also ire ich mich nicht.

So, am Donnerstag können wir sensationell anbieten 18 bis 20 Uhr.

Das liegt nicht an uns, das liegt an der Verfügbarkeit von Rollen.

Wäre unter diesen Bedingungen immer noch Interesse daran,

die Intensivübung auf den Donnerstag, okay. Also ich höre raus, das wird allgemein nicht gewünscht.

Ja gut, wir haben auch den anderen Raum vor sich selber noch nicht aufgegeben.

Okay, gut, das war das, das ging schnell.

So, und dann habe ich hier schon einen Tanz für die Evaluation.

Muss ich Ihnen das Verfahren noch erklären? Nein, das kennen Sie, ja?

Gut, also ich verteile die einfach.

Ja, wir kehren zurück zu den anderen technischen Dingen, nämlich zum Inhalt.

Wir haben jetzt gesehen, die vollständige Definition von Logik erster Stufe mit Syntax, Semantik und Beweistheorie.

So, nun sind wir ja Informatiker und wollen also gerne Maschinen anwerfen.

So wie wir das für Aussagen Logik ja letztlich auch tun.

Das Ding ist, mit Logik erster Stufe funktioniert das so uneingeschränkt nicht mehr.

Wir können das hier nicht zeigen, weil wir erstens keine Zeit haben

und zweitens, weil uns die Grundlagen dafür fehlen, die Sie jetzt im BFS gerade erst lernen.

Richtig, nicht?

Aber man kann es gleich wohl mal sagen, also Logik erster Stufe ist unentscheidbar.

Was bedeutet, also ich kann keinen Algorithmus bauen, der selbst wenn er sehr viel Zeit bekommt, um zu laufen,

mir für jede Formel in Logik erster Stufe nun sagt, ob die zum Beispiel erfüllbar ist oder nicht

oder meinetwegen gültig ist oder nicht, was sich leicht aufeinander reduzieren lässt.

Nichts desto weniger trotz gibt es erfolgreiche Beweiser, automatische für Logik erster Stufe,

sowas wie SPAS oder Vampire oder KR Hyper oder wie sie alle heißen.

Gut, das sind natürlich dann keine vollständigen Entscheidungsverfahren.

Typischerweise sind es Halbentscheidungsverfahren.

Das heißt, wenn es einen Beweis gibt und man sie aber Millionen Jahre laufen lässt,

dann finden Sie ihn irgendwann. Wenn es keinen Beweis gibt, dann werfen Sie eventuell nicht rechtzeitig das Handtuch.

Gibt aber auch Fälle, wo Sie sagen, okay, nicht beweisbar.

Gut. Ja, und in diese Algorithmik der Logik erster Stufe, auch wenn es uns eben kein volles Entscheidungsverfahren gibt,

wollen wir jetzt einsteigen. Und wir fangen an mit etwas Einfachem, was eben doch entscheidbar ist.

Also das ist dann nicht das Erfüllbarkeitsproblem, sondern ein viel, viel, viel, viel einfacheres Problem,

das man aber lösen muss, um nachher diese Beweise zu implementieren.

So, und zwar heißt das, so, jetzt was wir da hier...

Also das Problem, das wir heute lösen, lautet Unifikation.

So, es ist im Prinzip ein Problem, das wir alle aus der Mittelstufe kennen.

Ja, es handelt sich also um das Problem Gleichungen zu lösen, aber auf eine sehr eingeschränkte Art,

rein syntaktisch. So, was heißt das? Rein syntaktisch?

Nun, wir sehen eine Gleichung vor uns, das ist also einfach ein paar von Termen, zwischen die wir ein geeignetes Zeichen schreiben.

Für Zwecke der Unifikationsproblematik schreibe ich mal so einen Punkt über das Gleichheitszeichen.

Ich könnte den auch weglassen, aber dann entsteht immer Verwirrung und Verwechslung mit semantischer Gleichheit.

Damit ist das nicht zu verwechseln. Also, wir machen hier so ein besonderes Gleichheitszeichen, Gleichheit mit einem Punkt drüber.

Ja, wir wollen jetzt diese Gleichung lösen. Was soll das heißen?

Wir suchen eine Substitution Sigma, also etwas, was wir da einsetzen können. Das suchen wir auch sonst.

Also wenn wir zum Beispiel x² gleich 2 lösen wollen, dann suchen wir eine Zahl, die wir da einsetzen können für x,