Forschungsbericht 2005 - Max-Planck-Institut für Informatik

Automatisches Beweisen in komplexen Theorien

Automatic Theorem Proving in Complex Theories

Autoren
Sofronie-Stokkermans, Viorica
Abteilungen

Logik der Programmierung (Prof. Dr. Harald Ganzinger)
MPI für Informatik, Saarbrücken

Zusammenfassung
Wir erforschen Rahmenbedingungen, die es ermöglichen, Beweisaufgaben in komplexen Theorien modular in Beweisaufgaben für die einfacheren Bestandteile dieser Theorien zu zerlegen. Durch Ausnutzung der Modularität sind solche Beweisverfahren besonders flexibel und effizient und deshalb in vielen Bereichen (wie etwa in der Verifikation komplexer Systeme, aber auch in der Mathematik oder Wissensrepräsentation) anwendbar.
Summary
We identify situations in which it is possible to decompose proof tasks in complex theories in a modular way into proof tasks for the simpler components of these theories. As they exploit modularity, such proof procedures are especially flexible and efficient and are therefore widely applicable, for instance in the verification of complex systems, but also in mathematics or knowledge representation.

Die enorme Geschwindigkeit in der Entwicklung der Informationstechnik hat dazu geführt, dass heutzutage komplexe rechnergesteuerte Systeme fast überall eingesetzt werden: im Haushalt, in Autos, Zügen, Flugzeugen, Raketen oder Kraftwerken. Insbesondere in den letztgenannten sicherheitskritischen Bereichen können Softwarefehler katastrophale Folgen haben. Es ist deshalb sehr wichtig, das korrekte Funktionieren solcher Systeme zu garantieren, d.h. mathematisch zu beweisen. Die entstehenden Beweisverpflichtungen sind aber manuell allein schon wegen ihrer Größe nicht zu bewältigen. Darum ist es entscheidend, kritische Eigenschaften - sowohl in der Spezifikation wie in der Realisierung solcher komplexen Systeme - mit automatisierten Techniken, also mit Rechnerunterstützung, überprüfen zu können.

Eigentlich besteht der Traum der Wissenschaftler darin, solche Korrektheitsbeweise völlig automatisch vom Rechner durchführen zu lassen. Dieses Ziel ist aber in voller Allgemeinheit nicht erreichbar: es ist nicht möglich, ein Computer-Programm zu schreiben, welches das korrekte Funktionieren eines beliebigen Systems per Knopfdruck beweist. Dies geht bereits aus Resultaten von Gödel, Church und Turing aus der ersten Hälfte des letzten Jahrhunderts hervor. Für konkrete Anwendungsbereiche lassen sich jedoch effektive automatische Beweisverfahren angeben. Unsere Forschung beschäftigt sich mit der Frage, wie solche Verfahren wiederum effektiv kombiniert werden können.

Der erste Schritt beim rechnergestützten Beweisen ist die Formalisierung. Eigenschaften von konkreten komplexen Systemen sind normalerweise in natürlicher Sprache formuliert. Natürliche Sprache ist inhärent mehrdeutig. Deshalb ist es notwendig, die Systeme und die geforderten Eigenschaften mathematisch präzise mithilfe logischer Formeln zu beschreiben. Der eigentliche Beweis reduziert sich dann auf das Schlussfolgern über logische Formeln, so genannten Beweisaufgaben. Für manche Formelklassen lassen sich Entscheidungsverfahren angeben, d.h. jede beliebige Formel der Klasse kann effektiv bewiesen oder mit einem Gegenbeispiel falsifiziert werden.

Formeln, die konkrete komplexe Systeme beschreiben, gehören oft zu Klassen der Logik, für die Entscheidungsalgorithmen existieren. Da die Anzahl und Länge der Formeln, die in Anwendungen generiert werden, recht groß sein können, ist Entscheidbarkeit allein nicht immer ausreichend - eine möglichst niedrige Komplexität ist darüberhinaus äußerst wünschenswert. Es ist deswegen wichtig, anwendungs-relevante Theorien zu identifizieren, die (mit möglichst niedriger Komplexität) entscheidbar sind. Da komplexe Systeme Informationen über verschiedene Theorien enthalten, ist es sehr wichtig, effizient in kombinierten und damit komplexen Theorien schlussfolgern zu können.

Der Beitrag der Arbeitsgruppe ist ein Verfahren, welches es ermöglicht, Beweisen in komplexen Theorien auf das Beweisen in den Bestandteilen zu reduzieren. Entsprechend der Komplexität der anwendungsrelevanten Theorien werden hier Möglichkeiten besprochen, effiziente Beweisverfahren für (1) spezifische Theorien, (2) Theorieerweiterungen und (3) Theoriekombinationen zu entwickeln und anzuwenden. Das Verfahren ist recht allgemein und in vielen Bereichen (wie etwa in der Verifikation komplexer Systeme, aber auch in der Mathematik oder Wissensrepräsentation) anwendbar.

1. Effizientes Beweisen für spezifische Theorien

Um Rechner effektiv zum Beweisen benutzen zu können, ist es notwendig, Klassen von Formeln (oder Theorien) zu identifizieren, für die effiziente Entscheidungsalgorithmen existieren.

Beispiele: Dies können Formeln über konkrete Bereiche der Mathematik sein (z.B. Systeme von linearen Gleichungen oder Ungleichungen über ganze, rationale oder reelle Zahlen); über in der Logik wichtige Bereiche (wie Boole'sche Algebren) oder über Datenstrukturen, die in der Programmierung wichtig sind (z.B. Listen oder Arrays).

Für bestimmte Typen von Daten (etwa Zahlen) sind schon seit langer Zeit effiziente Entscheidungsverfahren bekannt. Aber auch Probleme über andere Datenbereiche können oft effizient gelöst werden. So haben viele Theorien die Eigenschaft, dass in der Suche nach einem Beweis oder Gegenbeispiel nicht alle Formeln, die die Theorie beschreiben, benutzt werden müssen, sondern nur solche, die den im Problem vorkommenden Formeln „hinreichend“ ähnlich sind. Das macht die Suche nach einem Beweis oder Gegenbeispiel viel einfacher; dadurch wird oft das Beweisen in polynomieller Zeit möglich.

Beim Beweisen von Eigenschaften doppelt verketteter Listen (wie z.B. die Eigenschaft, dass es keinen Knoten gibt, auf den zwei verschiedene Knoten verweisen), ist es ausreichend, die Liste lokal zu untersuchen (roter Kreis). Es spielt z.B. keine Rolle, welche Information in den Listenelementen gespeichert ist.

Theorien mit dieser Eigenschaft wurden von McAllester und Givan [1] und Ganzinger [2] studiert und entsprechenderweise „lokal“ genannt. Ganzinger und Basin [3] haben gezeigt, dass man oft automatisch erkennen kann, ob eine Theorie lokal ist oder nicht. Beispiele von lokalen Theorien
sind die Theorien einfach oder doppelt verketteter Listen (Abb. 1), die in der Verifikation von Sicherheitsprotokollen benutzten Theorien, die Kodierung bzw. Dekodierung mit bestimmten Schlüsseln formalisieren, sowie bestimmte Theorien aus der Wissensrepräsentation.

2. Hierarchisches Beweisen in Theorieerweiterungen

In Anwendungen kommen einzelne Theorien selten isoliert vor. So ist es oft notwendig, Erweiterungen einer gegebenen Theorie (hier als Basis oder Basistheorie bezeichnet) mit zusätzlichen Funktionen zu betrachten.

Beispiel: In der Mathematik ist es notwendig, über Funktionen mit numerischen Argumenten zu schließen; in der Logik über Funktionen zwischen geordneten Mengen oder Boole'schen Algebren; in der Softwareverifikation über Listen oder Arrays mit numerischen oder symbolischen Elementen, aber auch über Funktionen mit numerischen Argumenten.

Im Allgemeinen ist es problematisch, solche Erweiterungen zu behandeln, auch wenn effiziente Verfahren für die Basistheorie vorhanden sind. Manchmal ist es aber möglich, das ursprüngliche Problem zu einem Problem im Basisbereich zu reduzieren, welches dann mit einem spezialisierten Verfahren für die Basistheorie gelöst werden kann. Das allgemeine Prinzip eines solchen hierarchischen Verfahrens ist in Abbildung 2 dargestellt.

Prinzip des hierarchischen Schließens: Das ursprüngliche Problem (in der erweiterten Theorie) wird zu einem Problem in der Basistheorie reduziert, welches mit einem Verfahren für den Basisbereich gelöst werden kann.

Voraussetzungen, unter denen solche „hierarchische“ Verfahren ohne Informationsverlust anwendbar sind, wurden in unserer Gruppe von Ganzinger, Sofronie-Stokkermans und Waldmann [1,4] studiert. Genauso wie im Fall lokaler Theorien findet auch hier das Schließen über Erweiterungssymbole „lokal“ statt, was die Suche nach einem Beweis oder Gegenbeispiel beträchtlich erleichtert. Zahlreiche Erweiterungen von Datenbereichen in der Mathematik und Informatik haben diese Lokalitätseigenschaft. Ein Beispiel sind Erweiterungen mit freien oder monoton wachsenden Funktionen. Eine Funktion ist frei, wenn sie nicht durch zusätzliche Bedingungen eingeschränkt ist. Eine Funktion f - z.B. mit Zahlen als Argumente - ist monoton wachsend, wenn ihre Werte mit den Werten der Argumente wachsen, d.h. für alle Zahlen x, y gilt: falls x kleiner ist als y, so ist auch f(x) kleiner als f(y).

Diese Art von Erweiterungen kommen z.B. in parametrischen Ansätzen zur Verifikation reaktiver oder hybrider Systeme vor, wo die Veränderungen nicht explizit ausgedrückt, sondern als „Parameter“ benutzt werden (Abb. 3).

Ein Wasserstandsregler kann parametrisch modelliert werden, indem man die Veränderungen des Wasserspiegels beim Zufluss bzw. Abfluss von Wasser als Funktionen „in“ und „out“ darstellt, die von der Zeit und der Höhe des Wasserspiegels abhängen und zusätzliche Bedingungen erfüllen müssen.

Monotone Funktionen werden aber auch in der Wissensrepräsentation (etwa in terminologischen Datenbanken, wie sie zur Unterstützung intelligenter Suche im Internet gerade entwickelt werden), benutzt. Terminologische Datenbanken sind Datenbanken von Konzepten, die ausgehend von primitiven Konzepten definiert werden. Dazu ist es wichtig zu überprüfen, ob eine Datenbank widersprüchlich ist oder ob ein Konzept allgemeiner ist als ein anderes. Abbildung 4 gibt dazu ein Beispiel.

Terminologische Datenbank. Die Konzepte Enzym, Katalysator und Reaktion werden ausgehend von primitiven Konzepten (Protein, Prozess, Substanz) mithilfe der Konjunktion und der Konstruktoren „katalysiert“ und „erzeugt“ definiert. Dabei ist zu überprüfen, ob aus den Definitionen folgt, dass das Konzept Katalysator allgemeiner ist als das Konzept Enzym, d.h. dass jedes Enzym ein Katalysator ist.

Einige terminologische Datenbanken (z.B. die terminologische Datenbank für Medizin Snomed [5]) benutzen nur Konjunktion und sehr einfache zusätzliche Konstruktoren, um Konzepte zu definieren. Diese Konstruktoren können als monotone Funktionen modelliert werden. Die Argumente dieser Funktionen sind in diesem Fall nicht Zahlen, sondern Elemente aus dem Bereich der Konzepte, wo mit Begriffen wie „größer“ oder „kleiner“ ausgedrückt wird, dass ein Konzept allgemeiner bzw. spezieller ist als ein anderes. Für solche Datenbanken ist Widersprüchlichkeit in polynomieller Zeit (in der Größe der Datenbank) entscheidbar. Ebenso kann in polynomieller Zeit entschieden werden, ob ein Konzept allgemeiner oder spezieller ist als ein anderes [6]. Effiziente Entscheidungsverfahren, die auf lokalem bzw. hierarchischem Schlussfolgern basieren, sind in [4,7] beschrieben.

3. Modulares Beweisen in Kombinationen von Theorien

Selbst einfache Systeme können oft Informationen über mehrere Datenbereiche enthalten. So ist es in der Programmverifikation wichtig, im Stande zu sein, z.B. über Listen und Arrays mit numerischen Elementen zu schließen. Beim Studium von hybriden - oder Echtzeitsystemen muss zusätzlich zu den Datenstrukturen auch die Zeit modelliert werden. Die meisten in Anwendungen vorkommenden Systeme sind typischerweise Kombinationen einfacherer Systeme.

Beispiel: In der Verifikation komplexer, reaktiver oder hybrider Systeme ist die Koordinierung verschiedener Kontrollfaktoren ein Hauptproblem. In verteilten Datenbanken ist es oft notwendig, verschiedene Erweiterungen eines gemeinsamen Kerns mittels Konzepten und Konstruktoren zu betrachten.

Es gibt verschiedene Ansätze für das Schließen in komplexen Theorien. Ein sehr flexibler Ansatz ist das Ausnutzen von Modularität. Das ursprüngliche Problem wird in Teilaufgaben für die einzelnen Komponenten getrennt und für jede Teilaufgabe werden existierende spezialisierte Verfahren für die einzelnen Komponenten als „Blackbox“ benutzt. Die daraus resultierenden Einzellösungen werden dann wieder zu einer Gesamtlösung kombiniert. Diese Idee ist in Abbildung 5 dargestellt.

Prinzip des modularen Schliessens. Das Problem wird in Teilaufgaben zerlegt, die mit spezialisierten Beweisern gelöst werden. Ein Informationsaustausch zwischen den Beweisern für die Komponenten ist dazu notwendig.

So können zum Beispiel arithmetische Entscheidungsverfahren für rein numerische Teilaufgaben benutzt werden sowie effiziente Entscheidungsverfahren einzelner Datentypen für Teilaufgaben, die sich ausschließlich auf diese Datentypen beziehen. Dabei ist ein Informationsaustausch zwischen den jeweiligen Verfahren notwendig, um sicher zu sein, dass das Verfahren richtig entscheidet, ob eine Formel wahr ist oder nicht. Möglichkeiten für modulares Beweisen in Kombinationen von Theorien wurden in unserer Gruppe untersucht [8]; in [8] wird auch die Form der für den Informationswechsel notwendigen Formeln charakterisiert.

Das automatische Beweisen in komplexen Theorien ist eines der Forschungsgebiete in der Gruppe Logik der Programmierung am Max-Planck-Institut für Informatik. Die Forschungsergebnisse und Forschungsvorhaben der Gruppe auf diesem Gebiet sind zur Zeit eng mit den Zielsetzungen des SFB Transregio Projektes AVACS (Automatic Verification and Analysis of Complex Systems) verbunden. Im Rahmen dieses Projektes entwickeln wir effiziente Entscheidungsverfahren für verschiedene logische Theorien mit Anwendungen in der Verifikation komplexer Systeme. (Th. Hillenbrand, C. Ihlemann, S. Jacobs, V. Sofronie-Stokkermans, U. Waldmann. ).

Originalveröffentlichungen

1.
McAllester, D. und R. Givan.:
New results on local inference relations.
In: Principles of Knowledge Representation and Reasoning, Proc. of 3rd International Conference (KR'92), Morgan-Kaufmann Press 1992, 402 – 412.
2.
Ganzinger, H.:
Relating semantic and proof-theoretic concepts for polynomial time decidability of uniform word problems.
In: Proc. of 16th IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, New York 2001, 81-92.
3.
Basin, D. and H. Ganzinger:
Automated complexity analysis based on ordered resolution.
Journal of the ACM 48, 70-109 (2001).
4.
Sofronie-Stokkermans, V.:
Hierarchic reasoning in local theory extensions.
In: Conference on Automated Deduction, Lecture Notes in Artificial Intelligence 3632, Springer Verlag, Heidelberg 2005, 219 – 234.
5.
Spackman, K.A., K.E. Campbell, R.A. Cote:
SNOMED RT: A reference terminology for health care.
Journal of the American Medical Informatics Association, Fall Symposium Supplement, Hanley and Belfus, New York 1997, 640-644
6.
Bader, F.:
Terminological cycles in a description logic with existential restriction and terminological cycles.
In: G. Gottlob and T. Walsh (eds.), Proc. of 18th International Joint Conference in Artificial Intelligence, Morgan Kaufmann 2003, 325 – 330.
7.
V. Sofronie-Stokkermans:
Automated theorem proving by resolution in non-classical logics.
In: Proc. of the Fourth International Conference "Journées de l’Informatique Messine" – Knowledge Discovery and Discrete Mathematics (JIM 2003), INRIA Lorraine 2003. 151 -167.
8.
Ganzinger, H.,V. Sofronie-Stokkermans und U. Waldmann:
Modular proof systems for partial functions with weak validity.
In: D. Basin and M. Rusinowitch (eds.), Automated Reasoning. Second International Joint Conference, IJCAR 2004, Lecture Notes in Artificial Intelligence 3097, Springer Verlag, Heidelberg 2004, 168 – 182.
Zur Redakteursansicht