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

Ja, herzlich willkommen zur letzten Sitzung des Semesters. Ich beginne mit abschließenden Korrekturen.

Also man erinnere sich an REF, also Resolution with Implicit Factoring. Achtung, das ist eventuell

Klausurrelevant. Es ist allerdings eine technische Licklichkeit. Ich nehme die verallgemeinerte Form,

wo ich sowohl mehrere positive als auch mehrere negative Literale haben kann. Also irgendwie so.

So, wir bilden den MGU, dieser A1 bis AN und der B1 bis BK. Und als Resolvente kommt raus C Sigma D Sigma.

Soweit so korrekt. Damit die Regel tatsächlich vollständig wird, muss man Folgendes noch berücksichtigen.

Nämlich man muss vorher die variablen Mengen der beiden Klauseln, die man resolviert, desjunkt machen.

Man denkt, das muss man nicht, weil wir ja sowieso gesagt haben, dass in der Klauselmenge die Variablen

jeweils desjunkt sind zwischen zwei Klauseln. Das haut aber leider in einem Falle nicht hin,

nämlich dann, wenn man versucht, eine Klausel mit sich selber zu resolvieren. Das geht nämlich auch.

Mit sich selbst hat eine Klausel natürlich nicht desjunkte Variablen. Die Namen der Variablen,

die in diesen Klauseln vorkommen, die sind ja sowieso Schall und Rauch. Die kann ich umbenennen,

wie ich will. Und ich benenne die so um, dass da links und rechts verschiedene Variablen verwendet werden.

Das heißt, ich bin in der Klausel und habe hier sicherlich passar- in geben müssen. Assistant Ver(?)

Nehmen wir mal so eine Klausel hier. Die liest sich, wenn P von X gilt, dann gilt auch P von F von X.

Mit anderen Worten, P ist abgeschlossen unter F.

Dann packe ich mal was dazu, was nicht angehen kann. Also wenn mit X auch F von X in P ist, dann ist mit X auch F von F von X in P, 2x F angewandt.

Ich packe jetzt also mal eine Klausel rein. Moment, wie wollte ich das machen? Ich negiere das und nicht.

Das war's.

Ich packe jetzt mal was rein, was nicht angehen kann, nämlich ein Gegenbeispiel zu dem, was ich eben gesagt habe.

Ich nehme eine konstante A und ich verlange nicht P von A. Ich verlange P von A und ich verlange nicht P von F von F von A.

Das ist also etwas, was nicht angehen kann, nach dem, was ich gerade verargumentiert habe.

So, damit müsst ihr sich jetzt also hier die leere Klausel resolvieren lassen. Gehen wir den Kindern mal nummern.

Eins, zwei und drei. Wir resolvieren eins mit zwei. Dazu unifizieren wir.

Da sieht man das ja wieder nicht. Ich hatte mir das doch ausgedacht.

Also machen wir das einfacher. So, wir machen das jetzt einfacher.

Also ich resolviere das jetzt nicht bis zu Ende zum Widerspruch. Ich zeige nur, wie man eine Klausel erwartet, die man da kriegen will.

Nämlich, wie ich eben argumentiert habe. So, das hier ist eine daraus folgende Klausel. Die müsste also durch Resolutionen sich herstellen lassen.

Und wenn ich, und zwar eben, naja, ich habe ja nur eine Klausel, die müsste ich also mit sich selber resolvieren.

Ich jetzt versuche das Ding, ohne Variablenumbenennung, mit sich selber zu resolvieren.

Ja, dann müsste ich also unifizieren den mit dem. Das kann ich aber nicht, und zwar wegen o-curse-check.

Ja, dieses x kommt ja da wieder vor, in einem größeren Term. Da kann ich also einsetzen, wie ich will. Der bleibt immer größer als der da.

So, was ich jetzt also mache, ist, ich resolviere eins mit eins Strich. Ja, ich habe also hier den, das ist eins, und schreibe daneben...

Na, passt das hier nicht. Gut, ich schreibe ihn dann drunter.

Und hier ist eins Strich. Ja, also dasselbe Ding, nur mit der Variablenumbenannung. So, die haben jetzt das jüngte Variablen, ja, wie jetzt also der Typ da vorschreibt.

Und damit kann ich jetzt dann doch unifizieren, und zwar kann ich eben ein MGU finden, der x Strich substituiert durch f von x.

Also Sigma soll ja sein der MGU, der negativen Literale und der positiven Literale, die ich aufeinander matchen will.

Kommt also raus, x Strich wird substituiert durch f von x. So, wenn ich das mache, dann werden die beiden gleich. Die kann ich also gegeneinander resolvieren.

Übrig bleiben die beiden, aber der jetzt natürlich mit dieser Substitution. Ja, also raus kommt der Star.

So, da sieht man, warum man also diese Maßgabe nochmal braucht, beim Resolvieren variablen Missionen.

Zweitens, das Terminationswars der Unifikation. Danke noch einmal an den Herren in der ersten Reihe da,

der es wieder mal gemerkt hat, dass auch die Korrektur nicht stimmt.

Das interessiert vermutlich die meisten eher etwas weniger, daher also in der neuen Version des Skripts, wie sie jetzt online steht, da stimmt es hoffentlich.

Im Unterschied zum ersten sicher nicht klausurelevant. So, okay, sind noch Fragen zu dieser Geschichte mit der Resolution?

Keine? Gut, dann machen wir jetzt.

So, also viele englische Abkürzungen, damit ich mir nicht hier an der Überschrift schon die Fingerwunsch schreibe.

Die Ähnlichkeit der ND-Standardabkürzung für Natural Deduction, also natürliche Deduktion, natürliches Schließen in First Order Logic, also in Logik erster Stufe.

So, das ist also klassisches Material. Der ursprüngliche Vollständigkeitsbeweis stammt von Kurt Gödel, also derselbe, von dem auch die beiden berühmten Unvollständigkeitssätze stammen,

die sich aber, das ist jetzt kein Widerspruch, sondern die beziehen sich auf verschiedene Logiken. Und der Beweis, wie wir ihn jetzt präsentieren, der stammt also von Leon Henke.