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

Ja, herzlich willkommen. Vorweg zwei Ansagen. Zum einen, ich bin nächste Woche leider nicht da,

Herr Gonscharow wird mich vertreten. Zweitens, Sie finden auf dem nächsten Übungsblatt,

noch nicht ganz veröffentlicht, aber kommt heute eine Aufgabe. Die verwendet zunächst als Präsenzaufgabe,

das heißt, die müssen Sie nicht abgeben, einen halbautomatischen Theoreenbeweiser namens COG.

Ja, das ist schändlicherweise die französische Konkurrenz.

In diesem Theoreenbeweiser sollen Sie dann Beweise in diesem System des natürlichen Schließens,

das wir letztes Mal behandelt haben, in einem Werkzeug nachvollziehen.

Das ist also ein Beweiser, dem können Sie Stück für Stück die einzelnen Regeln sagen,

die Sie anwenden wollen. Gut, das verlangt, dass man sich ein bisschen die Syntax anguckt,

dazu gibt es also ein sogenanntes Cheatsheet im Netz von einem Andrej Bauer, nachdem man da vorgehen kann,

wo man also einzeln diese Regelanwendungen als sogenannte Taktiken wiederfindet.

Und man kann dann, wenn man die Beweise einmal auf Papier gemacht hat, das ist eine Aufgabe,

die jetzt schon, ich glaube, abzugeben ist, dann kann man die anschließend also im Theoreenbeweiser

nachbauen und sehen, dass das also wirklich da auch korrekt nachvollzogen wird.

Das ist natürlich nicht die Art, wie man normalerweise einen Theoreenbeweiser benutzt.

Die Art, wie man diesen Theoreenbeweiser benutzt, ist auf diesem Niveau noch, also mach mal und dann macht er das.

Das können die dann schon, das ist nichts in der Aufgabe.

Das sage ich jetzt schon deswegen, weil man natürlich, um diese Aufgabe zu lösen,

dieses System installiert haben muss.

Und es kann nicht schaden, das gleich nach Ende der Veranstaltung schon mal zu machen.

Auf den meisten anständigen Betriebssystemen ist das kein Problem.

Also auf meinem, naja, also schändlicherweise habe ich mittlerweile einen Mac,

deswegen weil die Batterie länger hält.

Also auf dem Mac zum Beispiel habe ich das gestern in 5 Minuten installiert

und auf Ubuntu geht es durch runterladen der entsprechenden Pakets ähnlich.

Und das dritte Betriebssystem ist mir egal.

Also das als Hinweis vorneweg.

Ja, gut, wir haben uns letztes Mal angesehen, diese Regeln des natürlichen Schließens

und wir haben mal pro Beheirat ein paar Beweise darin geführt

und auf den Aufgaben, auf dem neuen Aufgabenplatz sind jetzt also noch mehr Beweise zu führen,

dass man mal ein Gefühl dafür kriegt, wie diese Regeln ausgeführt werden.

Und wir hatten am Ende der Vorlesung bewiesen, dass diese Regeln korrekt sind.

Das heißt, es gilt, wenn ich eine Aussage aus gewissen Annahmen herleiten kann,

wenn ich also Psi aus Annahmen, die eine Menge groß V von Annahmen entgegensteigen,

bewiesen kann, dann ist Psi auch tatsächlich eine logische Folgerung aus groß V.

Das heißt, jede Wahrheitsbelegung, die alle Formeln in groß V wahrmacht,

also die alle meine Annahmen erfüllt, erfüllt auch die Formel Psi.

So, das war ein relativ leichter Beweis über Invertitionen.

Über die Beweislänge, wir haben ihn auch gar nicht vollständig gemacht,

sondern uns nur praktisch die schwierigste von denen, zu dem Zeitpunkt ja nicht so vielen Regeln rausgesucht

und das da beispielhaft durchgezogen.

Das nennt man Korrektheit auf Deutsch und ein englischer Termin, das hilft vielleicht auch.

Auf Englisch heißt das Soundness.

Und das ist so eine Mindestanforderung an ein Beweissystem, also jedes Beweissystem,

dass das nicht erfüllt, würde ich also an der Stelle dann sofort in die Tonne treten.

Ja, ein ganz anderes Kaliber ist folgende Aussage, die sogenannte Vollständigkeit.

Nämlich die umgekehrte Implikation, also wenn Psi eine logische Folgerung aus groß Phi ist,

wenn also jede Wahrheitsbelegung, die alle Formeln in groß Phi wahrmacht, auch Psi wahrmacht,

dann kann ich das in dem System auch beweisen.