1.4Aussagenlogik

Indirekter Beweis und Resolution

Den Widerspruch mechanisch suchen: Klauseln verschmelzen, bis die leere Klausel entsteht.

Leitformel
D1∨LD2∨¬LD1∨D2\frac{D_1 \lor L \qquad D_2 \lor \lnot L}{D_1 \lor D_2}
Lernziel

Indirekte Beweise führen, Formeln als Klauselmengen schreiben und mit dem Resolutionskalkül Unerfüllbarkeit nachweisen.

Lernpfad

Lernbausteine

0 von 7 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

  • Ein indirekter Beweis widerlegt die Negation des Ziels.
  • Eine Klausel ist ein ODER von Literalen; eine Klauselmenge wird mit UND verbunden.
  • Resolution entfernt LL und ¬L\neg L aus zwei Klauseln und vereinigt den Rest.
  • Die leere Klausel □\Box zeigt Unerfüllbarkeit und damit den gesuchten Widerspruch.
  • Eine faire Suche betrachtet alle nötigen Paare, obwohl die Reihenfolge der Schritte frei ist.

Interaktiv

Freies Experimentieren

Resolutions-Werkstatt: zwei Klauseln mit komplementärem Literal auswählen, die Resolvente bilden und die nummerierte Ableitung bis zur leeren Klausel □ fortsetzen.