Unification Algorithms for Boolean Rings

Abstract

We are interested in unification problems in free Boolean rings, i.e. we investigate equation solving over these structures. The two major issues are unification in free Boolean rings and unification in a combination of a free Boolean ring with free function symbols. For unification in free Boolean rings we present the two approaches, which are pursued by today's scientific community. We disclose the origin of those methods, explain and verify them and reveal their advantages and disadvantages. Finally the acquired knowledge is used to introduce several improvements to the implementation of the algorithms. The combination algorithm is a specific application of a more general algorithm operating on the combination of an arbitrary and a simple theory. Therefore besides describing the ideas and steps of the general algorithm, properties of the Boolean ring theory are utilized to build additional performance enhancing procedures into this algorithm. We receive a validation of this algorithm by comparing it to other algorithms of the relatively new field of combination algorithms.

In dieser Diplomarbeit werden Unifikationsprobleme in Bool'schen Ringen untersucht. Sie ist in zwei Teile gegliedert: Unifikation in freien Bool'schen Ringen, Unifikation in der Kombination eines freien Bool'schen Rings mit freien (uninterpretierten) Funktionssymbolen. Für die Unifikation in freien Bool'schen Ringen werden die beiden Ansätze präsentiert, die heutzutage in der Wissenschaft verfolgt werden. Wir geben Aufschluß über den Ursprung der Ansätze, erklären und verifizieren die Algorithmen und zeigen ihre Schwächen und Stärken auf. Die gewonnen Erfahrungen wurden genutzt, um weitere Verbesserungen in die implementierten Versionen einzubauen. Der Kombinationsalgorithmus ist eine spezielle Anwendung einer allgemeineren Prozedur, der die Kombination einer simplen und einer beliebigen Theorie behandelt. Die Ideen und Schritte des allgemeinen Algorithmus werden erklärt. Der Algorithmus wurde durch Einbau von Prozeduren weiterentwicklet, die spezielle Eigenschaften der Bool'schen Ringe ausnutzen. Die Einordnung des Algorithmus wird durch einen Vergleich mit anderen Algorithmen des relativen neuen Feld der Kombinationsalgorithmen gewonnen.