7.4 Beweise

Es ist möglich, sich den Beweisweg für eine beliebige Konklusion, die folgt, aus den Informationen zu suchen, die ein Venn-Diagramm liefert. Das erscheint auf den ersten Blick unwahrscheinlich, wo doch explizit in Venn-Diagrammen gar keine Regeln angewendet werden. Das war ja gerade der große Vorteil der Diagramme. Die Regeln der Booleschen Verbände stecken jedoch implizit in der Konstruktion der Diagramme und daher ist es, wenn eine Konklusion folgt, möglich, Beweise zu konstruieren. Der Beweis von Satz 3.3 zeigte, daß das immer geht. In der Tat sind die Beweise, die man so erzielen kann, nicht immer gerade sehr schön und Kleinigkeiten werden gelegentlich zu kompliziert bewiesen, aber dafür ist diese Beweismethode sehr schön algorithmisch.

Die Beweismethode ist bereits einmal beschrieben worden, und zwar, wie schon erwähnt, im Beweis von Satz 3.3. Wir werden die Beschreibung aber trotzdem noch einmal kurz wiederholen:

7.4.1 Halbordnungen

Halbordnungen (allgemeine Konklusionen) werden wie folgt bewiesen:

Es werden die Prämissen bestimmt, die Zellen streichen, welche die Konklusion betreffen. Diese Prämissen werden dann jeweils auf die Zellen spezialisiert, die Zellen der Konklusion sind. Dann werden die Zellen zusammengefaßt. Die dabei verwendeten Regeln sind die folgenden:

1.

$a \sqcup b \sqsubseteq c \dashv\vdash a \sqsubseteq c, b \sqsubseteq c$ (Satz 2.10)

2.

$a \sqsubseteq b \sqcap c \dashv\vdash a \sqsubseteq b, a \sqsubseteq c$ (Satz 2.10)

3.

$a \sqcap \overline{b} \sqsubseteq c \dashv\vdash a \sqsubseteq b \sqcup c$ (Satz 2.26, Transportationsregel von Peirce)

$a \sqcap b \sqsubseteq c \dashv\vdash a \sqsubseteq \overline{b} \sqcup c$ (Satz 2.26, Transportationsregel von Peirce)

4.

$a \sqsubseteq 0 \vdash a \sqcap b \sqsubseteq 0$ (Einfache Transitivitätsanwendung)

5.

$a \sqcap b \sqsubseteq 0, a \sqcap \overline{b} \sqsubseteq 0 \vdash a \sqsubseteq 0$ (Quine/McCluskey)

6.

$a \sqcup b = b \sqcup a$ (V2a)

$a \sqcap b = b \sqcap a$ (V2b)

Gegeben seien also beliebige Halbordnungen von Funktionen Boolescher Verbände.

Zunächst werden alle zum Beweis benötigten Prämissen in die Form $a \sqsubseteq b$ gebracht, dabei stehen auf der linken Seite nur Konjunktionen und auf der rechten nur Disjunktionen. Dieses geschieht mit den Regeln 1. und 2. durch Aufspaltung der Prämissen. Unter Umständen sind aber auch noch die DeMorgan Regeln und die Distributivgesetze notwendig. Dieser Schritt kann nahezu beliebig komplex sein (er kommt quasi einer Umwandlung in die disjunktive Normalform gleich nach Satz 2.29). Aus den Diagrammen ist dieser Schritt nicht ablesbar, weil er konstruktiv eliminiert ist. Daher ist der vom Venn-Programm gelieferte Beweis an dieser Stelle sehr kurz. Aber auch dieser Schritt ist algorithmisch, wie Satz 2.29 erkennen ließ.

Die so umgeformten Prämissen werden dann mit Hilfe der Transportationsregel von Peirce (3.) in Halbordnungen der Form $a \sqsubseteq 0$, d.h. in sog. 0-Subsumtionen verwandelt.

Mit Regel 4. werden die Prämissen soweit wie nötig spezialisiert. Soweit wie nötig heißt hier, daß bis auf die Ebene aller in der Konklusion und in den benötigten Prämissen enthaltenen Objekte spezialisiert wird, im Extremfall also bis auf die Ebene der Minterme.

Die auf die Zellen der Konklusion reduzierten Prämissen werden dann mit Hilfe von Regel 5. (Quine/McCluskey) zusammengefaßt.

Die so erzeugte Konklusion muß nun noch eventuell mit Hilfe der Regeln 1., 2. und 3. und evtl. noch DeMorgan und Distributivgesetze in die gewünschte Form gebracht werden. Auch dieser Schritt kann wieder extrem gekürzt sein.

Hier nicht extra aufgeführt sind kommutative Vertauschungen, die gelegentlich notwendig sind.

Der zugehörige Algorithmus ist sehr umfangreich, denn es wird in der Abfolge der obigen Regelanwendungen ein sehr komplexes Geflecht von Rück- und Querbezügen zwischen Listenelementen aufgebaut, die auf die Prämissen einer Konklusion verweisen, solange bis man bei den wirklichen Prämissen angelangt ist. Dann läuft nocheinmal ein Kürzungsalgorithmus über das Geflecht von Regelanwendungen, um unnötige Teile des Geflechts zu eliminieren.

Allgemeine Konklusionen können auch auf Streichungen beruhen, die durch Individualbegriffsdeklarationen hervorgerufen werden. Dann gehört noch mindestens eine partikuläre Prämisse mit zum Beweis. Diese partikuläre(n) Prämisse(n) wird (werden) im Beweis mit angegeben, sowie die allgemeinen Prämissen, die, falls vorhanden, dazu führen, daß die obige(n) partikuläre(n) Prämisse(n) zum Beweis gehören. Diese Streichungen können natürlich wiederum auf Individualbegriffsdeklarationen beruhen. Die Individualbegriffsdeklaration bringt eine Komplikation in die Beweismechanik, denn Schraffierungen von Zellen durch Individualbegriffsdeklarationen können wiederum auf Individualbegriffsdeklarationen beruhen, usw.  Dieses Problem wird durch einen rekursiven Aufruf der Beweisroutinen gelöst, bis keine Individualbegriffsdeklaration mehr als Prämisse auftaucht.

7.4.2 Negierte Halbordnungen

Negierte Halbordnungen (partikuläre Konklusionen) werden etwas anders als die allgemeinen Konklusionen bewiesen:

Es werden der Reihe nach die Sternsorten bestimmt, mit denen die Konklusion FOLGT. Dann werden die Sterne der jeweiligen Sternsorte bestimmt, die gestrichen sein müssen (möglicherweise muß keiner gestrichen sein). Die partikuläre Prämisse wird in ihre kleinsten Teile spezialisiert. Dann werden die gestrichenen Sterne entfernt und die übrigbleibenden Sterne zur Konklusion zusammengefaßt.

Es werden zusätzlich die folgenden Regeln benötigt:

7.

$a \sqcap \overline{b} \not\sqsubseteq c \dashv\vdash a \not\sqsubseteq b \sqcup c$ (Kontraposition von Satz 2.26)

$a \sqcap b \not\sqsubseteq c \dashv\vdash a \not\sqsubseteq \overline{b} \sqcup c$ (Kontraposition von Satz 2.26)

8.

$a \not\sqsubseteq 0 \vdash ( a \sqcap b ) \sqcup ( a \sqcap \overline{b} ) \not\sqsubseteq 0$ (Einfache kontraponierte Anwendung von (A5))

9.

$a \sqcup b \not\sqsubseteq 0, a \sqsubseteq 0 \vdash b \not\sqsubseteq 0$ (Satz 2.32)

10.

$a \sqcap b \not\sqsubseteq 0 \vdash a \not\sqsubseteq 0$ (Kontraposition von 4.)

Zunächst wird die benötige partikuläre Prämisse und (falls erforderlich) die benötigten allgemeinen Prämissen aufgelistet. Die partikuläre Prämisse wird mit Hilfe von Regel 7. in eine negierte 0-Subsumtionen verwandelt und dann mit Regel 8. bis auf Mintermstufe aufgespalten. Die allgemeinen Prämissen werden behandelt wie im Fall einer allgemeinen Konklusion. Dann werden mit Hilfe von Regel 9. die außerhalb der Konklusion liegenden gestrichenen Sterne der partikulären Prämisse entfernt. Die so entstandene negierte 0-Subsumtion wird sodann mit Regel 10. soweit wie nötig verallgemeinert und mit Regel 7. in die gewünschte Form gebracht.

Auch dieser Algorithmus ist wieder sehr kompliziert, enthält er doch zum Teil den Algorithmus für allgemeine Prämissen. Ansonsten funktioniert er aber ganz ähnlich, indem wieder entsprechend den anzuwendenden Regeln ein Geflecht von Rück- und Querbezügen aufgebaut und anschließend durchgekürzt wird.

Eine geeignete partikuläre Prämisse kann auch durch die Deklaration eines Individualbegriffes entstanden sein, in diesem Fall wird die entsprechende Deklaration als Prämisse angegeben.

7.4.3 Bemerkungen

Ein zuvor durchgeführter Konklusionentest, bei dem bereits wichtige Informationen gesammelt werden, zeigt, ob ein Beweis überhaupt möglich ist. Ist der Konklusionentest positiv, so folgt die Konklusion und dieses Wissen macht sich der Algorithmus zunutze. Er hat sozusagen eine Erfolgsgarantie. Das unterscheidet ihn von vielen anderen Beweisalgorithmen, die unter Umständen in die Irre laufen, weil sie etwas beweisen wollen, was nicht beweisbar ist.

Die Auffindung dieser Beweismechanik wurde durch die Verwendung des Halbordnungskalküls, gegenüber dem Booleschen Gleichungskalkül, begünstigt. Warum ?

Der Gleichungskalkül enthält im Prinzip nur eine Regel, nämlich die unglaublich starke Substitutionsregel. Diese Regel ist heuristisch sehr anspruchsvoll, sie verlangt in jedem Schritt eine ,,Idee``, was gleichzusetzen oder einzusetzen ist. Hier eine Beweismechanik zu finden, ist ziemlich schwierig, wenn nicht unmöglich, denn jeder Beweis ist anders. Der Halbordnungskalkül enthält dagegen eine ganze Reihe einfacher Regeln, von denen nur eine einzige etwas unangenehm ist, nämlich die Transitivitätsregel (A6). Bei der Rückwärtsentwicklung eines Beweises, d.h. der Konstruktion des Beweises von der Konklusion zu den Prämissen, ist man gezwungen einen ,,Mittelterm`` neu einzuführen, ebenfalls ein heuristisch sehr anspruchsvoller Akt.

Dieses Problem wird im vorliegenden Beweisalgorithmus umgangen, da die Transitivitätsregel nicht direkt zur Anwendung kommt. Statt dessen werden Sätze verwendet, die zwar mit Hilfe der Transitivitätsregel bewiesen wurden, aber nicht deren heuristisches Problem haben.

Der üblicherweise verwendete Gleichungskalkül zur Darstellung Boolescher Verbände verhindert gewissermaßen die Auffindung eines einfachen Beweisalgorithmus. Auch mit dem nackten Halbordnungskalkül ist es noch schwierig. Die ,,bildliche`` Darstellung des Halbordnungskalküls, sowie des Verhältnisses Prämissen - Konklusion im Venn-Diagramm macht das Erkennen der Zusammenhänge dagegen relativ einfach.

Die durch das Programm gelieferten Beweise beruhen quasi auf einem gegenüber dem Kalkül BV $^{\leq, \not\leq}$ veränderten Axiomensatz. Diese Kalküle sind jedoch äquivalent, denn die Kalküle des einen lassen sich in dem anderen beweisen.

Eine Richtung ist bereits erledigt durch die oben angegebenen Satznummern zu den verwendeten Regeln. Weiterhin sind die Axiome A7 und A8 durch die Übersetzung erledigt, die Gültigkeit der Axiome A6, A9 und A10 macht man sich leicht am Venn-Diagramm klar. Ebenso kann man sehr leicht die Gültigkeit von -A6- bis -A10- klären.

7.4.4 Individualbegriffe

Eine Individualbegriffsdeklaration als Konklusion wird behandelt, indem die Totalidentität mit einem bestehenden Individualbegriff nachgewiesen wird. Die Vorgehensweise entspricht also der bei allgemeinen Prämissen.

7.4.5 Aussagenlogik

Für die Aussagenlogik wird zusätzlich noch bei Bedarf das Urteilsprinzip angewendet. Das geschieht bevor die Prämissen in das Diagramm eingetragen werden und geschieht auch wieder beim Auslesen. Partikuläre Prämissen und Konklusionen, sowie Individualbegriffsdeklarationen sind in der Aussagenlogik weder sinnvoll noch möglich und können somit auch nicht behandelt bzw. bewiesen werden.

7.4.6 Grundformeln

Grundformeln (,,tautologische`` Urteile), wie z.B. $a \leq a$ sind mit Venn-Diagrammen nicht beweisbar, da sie in ihnen zwar eingetragen werden können, aber keinerlei sichtbare Auswirkungen zeigen. Sie sind bereits alle implizit in der Konstruktion der Venn-Diagramme enthalten. Das Programm kann nichts beweisen, da diese Konklusionen nichts streichen. Sie benötigen ja auch keine Prämissen, um zu folgen.