Logik

Als Teil meiner Dissertation benötige ich einen Algorithmus, der mir die ausgewogene Komposition eines komponentenbasierten Systems zeigt. Dies ist ein Bereich der Typtheorie. Da ich als Elektrotechniker damit vorher nicht wirklich etwas zu tun hatte, musste ich mich darin erst einarbeiten.

Kern dieses Teils ist ein Schnittstellenmodell bestehend aus statischem Teil, der definiert, was Schnittstellen sind und aus welchen Teilen sie bestehen. Hierzu zählen auch Relationen zur Vererbung und die Definitionen von Rückgabe- und Parametertypen. Das statische Schnittstellenmodell gibt also den Rahmen des "Machbaren" vor. Das dynamische Schnittstellenmodell besteht nun aus Methoden, die anhand eines konkreten statischen Models in der Lage sind gewisse Eingenschaften abzuleiten. Am Ende ist natürlich die oben erwähnte Ausgewogenheit der Konfiguration entscheidend.

Das dynamische Schnittstellenmodel basiert auf logischen Aussagen. Für die implementierung auf einem Computer bietet sich daher eine logische Programmiersprache an. Ich habe den Teil also in Prolog implementiert. Die Wissensbasis (also das statische Model) lässt sich sehr leicht aus den vorhandenen Schnittstellenbeschreibungen generieren. Das Regelsystem entspricht dem Algorithmus zur Ausgewogenheitsuntersuchung. Interessant sind nun einige Eigenschaften des Systems. Dazu muss man sich allerdings erst fragen, wie das ganze arbeitet.

Prolog ist eine logische Programmiersprache und basiert auf den Verfahren der Prädikatenlogik, die wiederum auf der Ausslagenlogik fusst. Als Einführung in das Themengebiet habe ich das Buch Aussagenlogik, Mengen Relationen gelesen und den Stoff mit Hilfe des Buches Logik im Klartext vertieft. Eine große Hilfe war auch das Buch von Prof. Lunze, in welchem insbesondere das Vorgehen von Theorembeweisern sehr schön erläutert wird.

Die Aussagenlogik befasst sich mit der Verknüpfung konkreter logischer Aussagen (boolsche Algebra) und legt dafür gewisse Gesetzmäßigkeiten fest. Die Prädikatenlogik erweitert dieses System, indem es auch Aussagen von allgemeiner Bedeutung zulässt.

Besonders wichtig ist die sog. Resolution. Dieses Verfahren gestattet es aus der bestehenden Wissensbasis neue Erkenntnisse abzuleiten, also zu schließen. Resolution wird in den Theorembeweisern für den Beweis einer Aussage benutzt. Allerdings wird dabei der sog. Widerspruchsbeweis geführt. Zur Wissensbasis wird dazu die negierte Aussage hinzugefügt und mit Hilfe der Resolution versucht die leere Klausel abzuleiten. Gelingt dies, ist die Aussage bewiesen.

Resolution ist sowohl in Aussagenlogik als auch in Prädikatenlogik korrekt, welches bedeutet, dass alle syntaktisch ableitbaren Erkenntnisse sich auch semantisch ergeben. Dummerweise ist die Resolution nur eingeschränkt vollständig. (Vollständigkeit bedeutet, dass alle semantisch ableitbaren Erkenntnisse sich auch syntaktisch ergeben.) Die Resolution ist aber widerlegungsvollständig, also vollständig in dem Falle des oben erwähnten Widerspruchbeises. (Siehe hierzu das Script von Prof. Büning). Bei allgemeingültigen Aussagen der Prädikatenlogik ist das Verfahren aber leider nicht entscheidbar, hört also mitunter niemals auf zu rechnen. Daher nutzt man in Prolog die eingeschränkt mächtige Ausdrucksweise der Horn-Klauseln. Unter der zusätzlichen Voraussetzung der Abgeschlossenheit (Closed-Wordl-Assumption) ist es einem Prolog Interpreter möglich nach spätestens N-Schritten nachzuweisen, ob eine Aussage wahr oder falsch ist.

Da es mitunter mehrere Möglichkeiten gibt bei der Resolution zum nächsten Zustand zu kommen, existieren diverse Verfahren, die dafür sorgen sollen, möglichst schnell zu einem Ergebnis zu gelangen. Das Ganze ist sehr nah mit der Graphensuche verwandt. Daher kann hier auch die Breiten- oder Tiefensuche verwendet werden, die aber relativ Zeitkomplex sind (exponentiell). Daher werden meist andere Strategien benutzt. Beispiele sind z.B. Unit-Preference-, Input-Preference- oder Set-of-support-Strategie. Die Unit-Preference Strategie mit Horn-Klauseln entscheidet dabei in linearer Zeit, ob eine Formel widerlegt werden kann. (Siehe Script von Prof. Büning, S. 94). Das dumme daran ist, dass das Verfahren nicht mehr vollständig ist.

Eine noch offene Frage ist: Was genau benutzt SWI-Prolog und wie sieht dort das Zeitverhalten aus?