Sequent Calculus #

Das Sequenzenkalkül dient dazu Theoreme möglichst genau abzubilden. Bereits in der Grundschule werden Theoreme bewiesen oder erklärt. Das Theorem “Die Summe der Innenwinkel eines Dreiecks beträgt 180 Grad” ist ein bekanntes Beispiel.

Sequent #

Ein Sequent ist ein generischer Name für etwas, dass wir beweisen wollen. Ein Beweis hängt immer mit mindestens einem Sequent zusammen. Ein Beispiel für ein Sequent ist “Es regnet” oder “es ist bewölkt”. Später sind Sequents oft von der Form \( H \vdash G \) und wird gelesen als Unter der Hyptothese H, beweise das Ziel G.

Proof Rules / Beweisregeln #

Beweisregeln werden verwendet, um Sequents zu beweisen. Die Beweisregel sieht ähnlich aus wie ein Bruch in der Mathematik. Dabei wird der Zähler Antecedent und der Nenner Consequent genannt. Hinter diesen Bruch schreibt man den Regelnamen. Es gibt aber auch viele andere Darstellungsformen. Hier wird der Gentzen Style verwendet

Der Antecedent Teil besteht aus einer endlichen und geordneten Liste von Sequents. Der Consequent Teil besteht aus einer Sequent. Der Consequent Teil ist bewiesen, sobald wir Beweise für alle Sequents im Antecedent Teil haben.

Bei einem vollständigen Beweis ist der Antecedent Teil also leer. Beweisregeln mit leerem Antecedent Teil nennt man auch Axiome. Diese muss man als gegeben/bewiesen annehmen.

Beispiele #

Theories #

Eine Theory oder calculus ist eine Menge von Proof Rules. Die obigen Beispiel könnten eine Theory bilden.

Proof / Beweis #

Ein Beweis ergibt einen Baum, der bei einem vollständigen Beweis ganz oben (im Antecedent Teil) keine Sequent mehr hat. Formal ist der Beweis vollständig wenn und nur wenn es keine pending sub-goals mehr hat. Im Beispiel unten ist kein vollständiger Beweis abgebildet, da das Sequent S7 nicht bewiesen wurde. S7 nennt man auch pending sub-goal.

Eine Sequent nennt man valide zur Theorie T, wenn und nur wenn es einen kompletten Beweis von der Sequent in T gibt.