Aussagenlogik: Deduktion und Algorithmen

Die Logik hat sich seit ihren Anfängen unter anderem mit der Präzisierung des Begriffs des Beweisens, also des logischen Schließens beschäftigt. Die heutigen technischen Möglichkeiten haben dazu geführt, daß verstärkt Fragen der maschinellen Verarbeitung im Vordergrund stehen. Auf der einen Seite ist daher die Verarbeitung der Logik von Interesse und auf der anderen Seite spielen die Prädikatenlogik und die Aussagenlogik als formale Beschreibungsmittel und als theoretisch fundierte Basis eine immer größere Rolle in der Informatik. Beispiele für die Anwendung dieser beiden Aspekte der Logik finden wir etwa in der Software-Verifikation und in der Logik-Programmierung.

Für viele Anwendungen bietet es sich an, Formeln einer bestimmten syntaktischen Struktur zu betrachten. Gründe für solche Normalformen können zum Beispiel die Übersichtlichkeit der Darstellung sein und damit verbunden eine relativ leichte Veränderbarkeit solcher Formeln oder die Anwendbarkeit dezidierter Algorithmen für Fragen der Folgerbarkeit und Widerspruchsfreiheit wie z.B. Resolutionsalgorithmen.

In diesem Kapitel behandeln wir das Erfüllbarkeitsproblem für die Aussagenlogik, d.h. das Problem, ob eine beliebig gegebene Formel erfüllbar ist.

In der Praxis sind nicht nur die Erfüllbarkeit von Formeln und die Algorithmen zu ihrer Entscheidung wichtig. Häufig steht auch die Frage im Vordergrund, ob aus einer logischen Beschreibung ein bestimmter Sachverhalt, d.h. eine weitere Formel gefolgert werden kann. Natürlich ist die semantische Folgerbarkeit mit dem Umweg über die Erfüllbarkeit beantwortbar, indem wir das Deduktionstheorem für ⊨ ausnutzen, d.h. die Äquivalenz „α ⊨ β ⇔ (α Λ ¬β) nicht erfüllbar“.

Wie wir bisher gesehen haben, ist das Schlußfolgern in der Aussagenlogik — selbst wenn wir Formeln in Konjunktiver Normalform betrachten — im schlechtesten Fall eine aufwendige und komplexe Angelegenheit. Es stellt sich ganz natürlich die Frage nach Teilklassen der Aussagenlogik, die noch eine vernünftige, d.h. nicht-triviale Ausdruckskraft besitzen, aber eine schnelle Bearbeitung zulassen. Eine solche Teilklasse wollen wir in diesem Kapitel betrachten. Sie ist nach A. Horn benannt, der sich zuerst mit diesen Formeln (für die Prädikatenlogik) beschäftigt hat. Die Klasse der Horn-Formeln um-faßt alle Formeln in Konjunktiver Normalform, deren Klauseln sich als Implikationen zwischen positiven Literalen als Prämisse und (maximal) einem positiven Literal als Konklusion darstellen lassen. Diese recht übersichtliche Form von „wenn-dann-Aussagen“ kann sicherlich als ein Grund für den erfolgreichen Einsatz von Wissensrepräsentationen angesehen werden, die auf Horn-Formeln basieren.

In den bisherigen Kapiteln haben wir verschiedene Algorithmen für den Test auf Erfüllbarkeit von Formeln vorgestellt und analysiert. Desweiteren haben wir die Resolution als mächtigen Kalkül für die Verarbeitung von Formeln in Konjunktiver Normalform, speziell für Horn—Formeln kennengelernt. Allerdings ist dieser Kalkül nur widerlegungsvollständig. Es läßt sich mit Hilfe der Herleitungsregeln nur feststellen, ob eine Formel widerspruchsvoll ist.

In diesem Kapitel werden wir aussagenlogische Formeln behandeln, die zusätzlich Quantoren über Atome enthalten. Bevor wir eine Definition dieser Formelklasse angeben, wollen wir anhand einiger Beispiele die Möglichkeiten quantifizierter aussagenlogischer Formeln verdeutlichen. Da die Quantoren sich über Atome erstrecken, erhalten diese den Charakter von Variablen. Anstelle von Atomen sprechen wir daher in diesem Kapitel in der Regel von (aussagenlogischen) Variablen.