Guten Morgen.

Als erstes, wir haben, vielen Dank, ein echtes Kalaha-Spiel, also fast echtes Kalaha-Spiel.

Das kann man sehr schlecht zeigen, ohne hier eine Riesenschweinerei zu bauen.

Deswegen gucken Sie sich das in der Pause vielleicht an.

Und zwar ist das kein ganz echtes Kalaha-Spiel, weil eigentlich müssten diese hier vereinigt sein.

Weil das die jeweiligen... Wie nennt man die?

Wie nennt man ja ein eigenes Kalaha-Spiel?

Also diese beiden da, wo man seine eigenen Steinchen reinschmeißt letztlich.

Und das ist eigentlich ein ganz klarer Vorbild oder so ähnlich? Also ist das irgendwie so eine Abfallspielung?

Bisschen anders.

Genau, es ist tatsächlich eines der ältesten Spiele der Menschheit.

Insofern kann man sich vorstellen, dass man in den 4000 Jahren oder 5000 Jahren, in denen das bereits gespielt wird,

dass die Leute da auf viele Ideen gekommen sind.

Aber im Prinzip geht es um in etwa so etwas.

Und man kann auch Tribal Color Heart damit spielen, wenn man sich die beiden letzten Dinge virtuell vereinigt.

Gut.

Des Weiteren sind wir längst jenseits Gameplay und hatten uns mit Logik beschäftigt.

Und hatten uns insbesondere Tablone und Resolutions Kalküle angeguckt.

Heute ist irgendwie der Plan, dass wir uns im wesentlichen Vollständigkeit von einem dieser beiden angucken.

Es ging dabei bei den Tablos darum, dass wir einen Test Kalkül haben,

indem wir die Allgemeingültigkeit einer Formel zeigen, indem wir nach dem Unerfüllbarkeitstheorem die Unerfüllbarkeit ihrer Negation testen.

Deswegen Test Kalkül.

Und wir verwenden eine spezielle Ausprägung dieses Test Kalküls, indem wir nämlich gelabelte Formeln verwenden,

indem wir nämlich jeweils eine Formel mit ihrem intendierten Wahrheitswert labeln.

Und deswegen haben wir sowas von der Bauart P und Q true oder so etwas.

Andere Arten das aufzuschreiben, sind indem man hier sagt P und Q und hier nicht P.

Und hier kann man sagen Aussagenvariabeln und ihre Negationen sind literale, während wir hier Aussagenvariabeln mit Label Literale nennen.

Das ist Jacke wie Hose im Prinzip.

Und ich persönlich finde dieses hier ein bisschen schöner und mache das deswegen so.

Wie funktioniert also Tablos?

Wir werden die Formel mit einem Falls ansehen und analysieren sie mit fünf Regeln in so einem Baum.

Und zwar so lange bis es saturiert ist.

Das heißt wir können keine Regel anwenden, die uns neues Zeugs gibt.

Und dann gucken wir nach, ob jeder dieser Äste geschlossen ist.

Und schließen tun wir die, indem wir elementare Widersprüche finden.

Jeder Ast in diesem Tableau entspricht einer Variablenbelegung.

Und wenn er geschlossen ist, kann es keine Variablenbelegung geben.

In diesem Fall nämlich weil P nicht gleichzeitig falsch und wahr machen kann.

Und der Trick an der ganzen Sache ist, wir versuchen Belegungen zu finden, die dieses Ding hier falsch macht.

Scheitern grandios.

Und wenn wir daran scheitern, das ist falsch zu machen, muss es wohl für alle Belegungen wahr sein.

Das ist die Idee eines Testkalkül.

Nun kann man sich fragen, was machen eigentlich Menschen?

Und wenn wir gesagt haben, beweisen Sie bitte Laberlisch-Wall irgendwas, dann kommt sicherlich kein Tableau typischerweise.

Deswegen möchte ich einen Nicht-Test-Kalkül noch eben einführen.

Den sollten die meisten von Ihnen schon gesehen haben. Das ist der Kalkül des natürlichen Schließens.

Der ist auch schon 80 Jahre alt und der ist dafür gemacht, nachzuspüren, wie Menschen Schlüsse ziehen und Begründungen machen.

Und die machen das garantiert nicht mit einem Testkalkül.

Und heraus kommt ein Kalkül dieser Bauart, der vorwärts schließt.

Wir haben Axiome, in diesem Fall genau eins, nämlich das Tertium Nondatur, A oder nicht A.