Applications for Symbol Elimination in Combination With Hierarchical Reasoning

Summary The goal of this PhD thesis is to investigate possibilities of using symbol elimination for solving problems over complex theories and analyze the applicability of such uniform approaches in different areas of application, such as verification, knowledge representation and graph theory. In the thesis we propose an approach to symbol elimination in complex theories that follows the general idea of combining hierarchical reasoning with symbol elimination in standard theories. We analyze how this general approach can be specialized and used in different areas of application. In the verification of parametric systems it is important to prove that certain safety properties hold. This can be done by showing that a property is an inductive invariant of the system, i.e., it holds in the initial state of the system and is invariant under updates of the system. Sometimes this is not the case for the condition itself, but for a stronger condition it is. In this thesis we propose a method for goal-directed invariant strengthening. In knowledge representation we often have to deal with huge ontologies. Combining two ontologies usually leads to new consequences, some of which may be false or undesired. We are interested in finding explanations for such unwanted consequences. For this we propose a method for computing interpolants in the description logics EL and EL+, based on a translation to the theory of semilattices with monotone operators and a certain form of interpolation in this theory. In wireless network theory one often deals with classes of geometric graphs in which the existence or non-existence of an edge between two vertices in a graph relies on properties on their distances to other nodes. One possibility to prove properties of those graphs or to analyze relations between the graph classes is to prove or disprove that one graph class is contained in the other. In this thesis we propose a method for checking inclusions between geometric graph classes. Zusammenfassung Das Ziel der vorliegenden Doktorarbeit ist die Untersuchung von Möglichkeiten zur Anwendung von Symbolelimination, um Probleme über komplexen Theorien zu lösen, sowie die Analyse der Anwendbarkeit solcher einheitlichen Ansätze in verschiedenen Anwendungsbereichen, beispielsweise in der Verifikation, Wissensrepräsentation oder Graphentheorie. In der Arbeit stellen wir ein Verfahren für die Symbolelimination in komplexen Theorien vor, welches der generellen Idee folgt, hierarchisches Schließen mit Symbolelimination in Standardtheorien zu verbinden. Wir untersuchen, wie dieser allgemeine Ansatz spezialisiert werden kann, um ihn in verschiedenen Anwendungsgebieten zu verwenden. In der Verifikation parametrischer Systeme ist es wichtig zu beweisen, dass bestimmte Sicherheitsbedingungen erfüllt sind. Dies kann erreicht werden, indem man zeigt, dass eine Bedingung eine induktive Invariante des Systems ist, das heißt, dass sie im Anfangszustand des Systems erfüllt ist und unter Veränderungen des Systems erhalten bleibt. Manchmal ist dies für die Bedingung selbst nicht der Fall, aber für eine stärkere Bedingung schon. In der Arbeit stellen wir eine Methode zum zielgerichteten Verstärken von Invarianten vor. In der Wissensrepräsentation wird häufig mit großen Ontologien gearbeitet. Das Zusammenfügen zweier Ontologien bringt für gewöhnlich neue Konsequenzen mit sich, von denen einige womöglich fehlerhaft oder unerwünscht sind. Wir sind interessiert daran, Erklärungen für das Auftreten solcher unerwünschter Konsequenzen zu finden. Zu diesem Zweck stellen wir eine Methode vor, mit der Interpolanten in den Beschreibungslogiken EL und EL+ generiert werden können, basierend auf einer Übersetzung zur Theorie der Halbverbände mit monotonen Operatoren und einer bestimmten Form von Interpolation in dieser Theorie. In der Forschung zu kabellosen Übertragungsverfahren beschäftigt man sich mit Klassen von geometrischen Graphen, bei denen die Existenz oder Nicht-Existenz einer Kante zwischen zwei Knoten im Graph von Eigenschaften auf deren Distanzen zu anderen Knoten abhängt. Eine Möglichkeit, um Eigenschaften solcher Graphen zu beweisen oder Beziehungen zwischen zwei Klassen zu analysieren, ist zu zeigen, dass eine Klasse in der anderen enthalten ist. In dieser Arbeit stellen wir eine Methode vor, um die Inklusion einer Klasse von Graphen in einer anderen zu überprüfen.