Seite parallel anzeigen





Der Sequentialkalkül

(Aussagenlogik Kapitel 7.2.1)

Diese Seite nimmt Bezug auf

(Seite parallel anzeigen)
Liste überspringen
Zum Seitenanfang

Der Sequentialkalkül beweist, dass eine Formel γ aus einer Formelmenge Γ ableitbar ist, indem ein Ausdruck der Form Γ|--γ abgeleitet wird. Γ|--γ wird als "Sequent" bezeichnet.
Es gibt Sequentialkalküle (auch "Sequenzenkalküle") für verschiedene Logiken - wir wollen hier eine vereinfachte Version eines klassischen Sequentialkalküls (auch "LK" für "Logikkalkül Klassisch") für die Aussagenlogik betrachten, wobei wir annehmen, dass alle materialen Äquivalenzen und -Implikationen der Formeln eliminiert wurden.
 
Der (hier vorgestellte) Sequentialkalkül enthält
  • 1 Axiomenschema: Γ,γ|--δ|γ
  • die folgenden Schlussregeln (das/die Sequent(e) oberhalb des Striches sind die Voraussetzungen für die Regelanwendung, das Sequent unterhalb des Striches das Ergebnis der Regelanwendung):
    !-links:
    Γ|--δ|γ
    Γ,!γ|--δ
    !-rechts:
    Γ,γ|--δ
    Γ|--δ|!γ
    &-links:
    Γ,γ,δ|--λ
    Γ,γ&δ|--λ
    &-rechts:
    Γ|--λ|γ     Γ|--λ|δ
    Γ|--λ|γ&δ
    |-links:
    Γ,γ|--λ     Γ,δ|--λ
    Γ,γ|δ|--λ

Beispiel - Eine Ableitung im Sequentialkalkül

Wir wollen das Sequent (a|b)&!a|--b ableiten:
Beschreibung der Ableitungsschritte
  • Wir bilden eine Instanz des Axioms und
  • wenden die !-links Schlussregel an,
  • fügen ein weiteres Axiom hinzu und
  • wenden die |-links Schlussregel an.
  • Schlussendlich wenden wir die &-links Schlussregel an und
  • erhalten das gewünschte Sequent.
Ableitung (fahre mit der Maus über die Sequente, um etwas über ihre Herleitung zu erfahren)
a|--b|a
a,!a|--b b,!a|--b
a|b,!a|--b
(a|b)&!a|--b
Die Ableitung kann als Ableitungsbaum gesehen werden.
Da eine Ableitung von den Axiomen zu den Endsequenten sehr aufwendig ist (die Axiome müssen "erraten" werden), werden solche Ableitungen normalerweise von unten nach oben gebildet: das Sequent wird so lange zerlegt, bis auf jedem Ast ein Axiom erreicht wird.

Der Sequentialkalkül hat folgende Eigenschaften:
  • Er hat 1 einfaches Axiomenschema.
  • Er hat viele, eng semantisch orientierte Regeln.
  • Er ist vollständig und korrekt.
  • Gilt ein Sequent, so führt jede Abfolge von Zerlegungen zu Axiomen ("don't-care-Indeterminismus").
  • Er ist analytisch, da nach einer Zerlegung eines Sequents, die neuen Sequente nur aus Teilformeln des ursprünglichen Sequents bestehen.