Ja, herzlich willkommen.

Wir haben letztes Mal eine Methode kennengelernt, mit deren Hilfe wir die verschiedenen Schlussfolgerungsprobleme,

die sich in der Aussagenlogik stellen, im Prinzip lösen können.

Wir können also feststellen, ob eine Formel erfüllbar ist, ob sie gültig ist, ob sie logische Folgerungen aus irgendwelchen Annahmen ist.

Das alles, indem wir diese Wahrheitstafelmethode verwenden, die wir also am Ende der letzten Sitzung ausprobiert haben, an sehr, sehr einfachen Beispielen.

Dass diese Beispiele sehr, sehr einfach waren, hatte seinen Grund.

Die Beispiele hatten also im schlimmsten Falle zwei propositionale Atome.

Bei einem propositionalen Atom, fangen wir mal an,

bei einem propositionalen Atom muss ich in der Wahrheitstafel zwei Zeilen hinschreiben.

Also eine für den Fall, dass es wahr ist, und eine für den Fall, dass das propositionale Atom falsch ist.

Bei zwei Atomen sind es schon vier Zeilen.

Da muss ich vier Kombinationen durchprobieren für die Wahrheitswerte der beiden Atome.

Bei drei propositionalen Atomen sind es schon acht Zeilen.

Sie sehen, wo das hinläuft.

Die Wahrheitstafel ist im Allgemeinen exponentiell lang.

Das heißt, spätestens ab der Stelle, wo ich so etwas wie konservativ zehn propositionale Atome habe,

ist das nicht mehr wirklich machbar.

Bei zehn propositionalen Atomen hat die Wahrheitstafel 1024 Zeilen.

Das möchte niemand mehr machen.

Wir brauchen also intelligentere Methoden, um Erfüllbarkeit und Schlussfolgerung und derlei in Aussagenlogik zu entscheiden.

Wir werden im Laufe der Veranstaltung zwei Methoden dafür kennenlernen.

Eine, die noch sehr von Hand normalerweise gehandhabt wird, und die kommt heute,

das ist die Methode des natürlichen Schließens.

Wir werden noch eine weitere Methode kennenlernen.

Das ist die sogenannte Resolutionsmethode.

So, wir beginnen, wie gesagt, mit

mit

mit natürlichem Schließen.

mit

Gut, wir werden also jetzt ein formales System hinschreiben.

und ein formales System besteht typischerweise aus zwei wesentlichen Zutaten,

erstens aus Regeln und zweitens aus Aktionen.

Da besteht ein fundamentaler Unterschied zwischen Regeln und Aktionen.

Schreiben wir mal eine Regel hin, die wir im Wesentlichen schon gesehen haben, das ist diese hier.

Die ist hier.

Und dann kommt der erste Schließens.

Das ist die Schließensmethode.

Das ist ein Schließensmethode, das wir jetzt hier an der Seite sehen.

Das ist die Schließensmethode, die wir jetzt hier sehen,

die wir jetzt hier sehen, die wir hier sehen.

Und dann kommt der zweite Schließensmethode.

Das ist Regeln und Aktionen. Schreiben wir mal eine Regel hin, die wir im Wesentlichen schon gesehen haben, das ist diese hier.

So Regeln schreiben wir typischerweise mit so einem Bruchstrich, wenn man will.

Oberhalb dieses Bruchstrichs stehen eine oder mehrere Formeln oder vielleicht auch mal gar keine.

Das sind die sogenannten Prämissen der Regel. Und unter dem Bruchstrich steht nur eine Formel und

diese Formel nennt man die Konklusion. Und was die Regel uns sagt ist, wenn wir

die Formeln, die oberhalb des Strichs stehen, also die Prämissen, wenn wir die

schon hergeleitet haben, dann dürfen wir, vermöge dieser Regel, die Konklusion

ebenfalls herleiten.

Das ist so eine Generationenfrage. Wie viele von Ihnen kennen noch das Buch