© 1999 François Bry
Dieses Lehrmaterial wird ausschließlich zur privaten Verwendung angeboten. Eine nichtprivate Nutzung (z.B. im Unterricht oder eine Veröffentlichung von Kopien oder Übersetzungen) dieses Lehrmaterials bedarf der Erlaubnis des Autors.


4.2 Entscheidbarkeitsergebnisse für die Aussagenlogik

Die Tatsache, dass der Algorithmus folgt(F,G) für aussagenlogische Formeln F und G korrekt und vollständig ist, bedeutet insbesondere, dass die Folgerungsbeziehung für die Aussagenlogik entscheidbar ist.

Entsprechende auf Wahrheitstabellen aufbauende korrekte und vollständige Algorithmen sind für andere semantische Begriffe genauso offensichtlich wie für die Folgerungsbeziehung. Damit gilt:

Satz 4.2.1 (Entscheidbarkeit im endlichen Fall).   Die Unerfüllbarkeit einer aussagenlogischen Formel oder einer endlichen Menge von aussagenlogischen Formeln ist entscheidbar. Ebenso die Erfüllbarkeit, Falsifizierbarkeit, Allgemeingültigkeit.

Satz 4.2.2 (Semi-Entscheidbarkeit im unendlichen Fall).   Die Unerfüllbarkeit einer unendlichen, aber aufzählbaren Menge von aussagenlogischen Formeln ist semi-entscheidbar.

Beweis:   Sei S eine aufzählbare, unendliche Menge von aussagenlogischen Formeln. Es gibt also einen Algorithmus FormelS(i), der eine natürliche Zahl als Argument hat, für jedes Argument terminiert und eine Formel aus S als Ergebnis liefert, derart dass S = {FormelS(i) | i∈N}.

Dieser Algorithmus ist eine Repräsentation der unendlichen Menge S, und deshalb ist er das Argument des zu konstruierenden Algorithmus für die Unerfüllbarkeit.

Algorithmus   unerfüllbar(FormelS):
  1. Initialisierung: i:=0 und Si:=∅.
  2. Schleife:

    1. Si:=Si∪{Formel}S(i)
    2. Falls Si unerfüllbar ist: Schleifenabbruch, liefere Ergebnis ja
      andernfalls i:=i+1 und Fortsetzung der Schleife.

Jedes in der Schleife gebildete Si ist eine endliche Teilmenge von S. Die Unerfüllbarkeit von Si in Schritt 2(b) ist also nach dem vorigen Satz entscheidbar. Sowohl Schritt 2(a) als auch Schritt 2(b) terminiert.

Wir betrachten zunächst den Fall, dass die durch FormelS repräsentierte unendliche Menge S erfüllbar ist. Da jede Teilmenge einer erfüllbaren Menge ebenfalls erfüllbar ist, wird die Schleife für kein i abgebrochen. Das heißt, unerfüllbar(FormelS) terminiert für erfüllbares S nicht.

Falls S unerfüllbar ist, gibt es nach dem Endlichkeits- oder Kompaktheitssatz für die Aussagenlogik (Satz 3.3.9) eine erfüllbare endliche Teilmenge von S. Sei {FormelS(i1),...,FormelS(ik) } eine solche Teilmenge, und sei m das Maximum der Indizes i1,...,ik. Im Schleifendurchgang mit i=m enthält Si also die unerfüllbare Teilmenge {FormelS(i1),...,FormelS(ik)} und ist damit selbst unerfüllbar. Damit wird spätestens für i=m die Schleife beendet und das Ergebnis ja geliefert.

Da der Algorithmus das Ergebnis nein gar nicht liefert und das Ergebnis ja nur bei unerfüllbarem S, ist er korrekt. Außerdem ist er vollständig bezüglich der Unerfüllbarkeit, aber nicht bezüglich der Erfüllbarkeit.

Dieser Semi-Entscheidungs-Algorithmus für die Unerfüllbarkeit ist selbstverständlich kein Beweis dafür, dass es keinen Entscheidungs-Algorithmus gibt, der auch für erfüllbares S terminiert (und zwar mit dem Ergebnis nein). Das folgende Beispiel liefert wenigstens eine anschauliche Begründung dafür.

Angenommen, die erste Formel in der Aufzählung von S ist ¬p. Es könnte sein, dass an einer Stelle k in der Aufzählung auch die Formel p vorkommt. In diesem Fall kann man die Unerfüllbarkeit im k-ten Schritt feststellen, ohne die (unendlich vielen) weiteren Formeln betrachten zu müssen. Wenn man aber die Formeln bis zu einer Stelle k in der Aufzählung betrachtet hat, ohne dass p vorgekommen ist (und ohne dass ein anderer Grund für die Unerfüllbarkeit aufgetreten ist), weiß man nicht, ob p vielleicht später noch vorkommt. Das Nicht-Vorkommen der Formel p in der Aufzählung kann man an keiner Stelle feststellen, ohne die (unendlich vielen) weiteren Formeln zu betrachten. Alle Formeln der Aufzählung zu betrachten ist aber mit endlich vielen Schritten nicht möglich.

Es gibt hinreichende Kriterien für die Erfüllbarkeit in Spezialfällen. Man kann den Algorithmus so erweitern, dass er in derartigen Spezialfällen das korrekte Ergebnis nein liefert. Aber derartige Kriterien können nicht alle erfüllbaren Fälle abdecken.

Validierung