1.5Aussagenlogik

Korrektheit und Vollständigkeit

Beweist ein Kalkül nur Wahres – und alles Wahre? Für die Aussagenlogik lautet die Antwort zweimal ja.

Leitformel
⊢φ⟺⊨φ\vdash \varphi \quad \Longleftrightarrow \quad \models \varphi
⊢φ\vdash \varphi⟺⊨φ\Longleftrightarrow \models \varphi
Lernziel

Korrektheit und Vollständigkeit eines Kalküls unterscheiden, die Sätze für die drei Kalküle kennen und SAT als schweres Problem einordnen.

Lernpfad

Lernbausteine

0 von 6 erledigt

Jeder Baustein enthält eine Erklärung und eine Kurzfrage. Beispiele und Labore machen die Regeln sichtbar. Richtig beantwortet, wird der Baustein automatisch abgehakt.

Tipp: Arbeite die Bausteine der Reihe nach durch.

Auf einen Blick

  • Korrektheit: ⊢φ⇒⊨φ\vdash\varphi\Rightarrow\models\varphi.
  • Vollständigkeit: ⊨φ⇒⊢φ\models\varphi\Rightarrow\vdash\varphi.
  • Für Aussagenlogik sind Wahrheitstabellen, geeignete Hilbert-Kalküle und Resolution korrekt und vollständig.
  • Endlich viele reduzierte Klauseln sichern Terminierung einer systematischen Sättigung, aber keine kurze Laufzeit.
  • SAT ist NP-vollständig; ob P = NP gilt, ist offen.

Interaktiv

Freies Experimentieren

Zwei Welten nebeneinander: links das Beweisbare (⊢), rechts das Wahre (⊨) – Korrektheit und Vollständigkeit als Pfeile dazwischen, dazu ein Zähler für die 2ⁿ Belegungen, die SAT so teuer machen.