Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-42862
Titel: | Unification Algorithms for Boolean Rings |
VerfasserIn: | Crone-Rawe, Bernard |
Sprache: | Englisch |
Erscheinungsjahr: | 1989 |
Erscheinungsort: | Kaiserslautern |
Freie Schlagwörter: | Boolean ring Boolean algebra Unification Equational Theories Theory-unification Combination of Equational Theories Theorem Prover Bool'sche Ring Bool'sche Algebra Unifikation Gleichheitstheorie Theorieunifikation Kombination von Gleichheitstheorien Automatischer Beweiser |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
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. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-428628 hdl:20.500.11880/38557 http://dx.doi.org/10.22028/D291-42862 |
Schriftenreihe: | SEKI working paper : SWP ; SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1860-5931] |
Band: | 89,1 |
Datum des Eintrags: | 30-Sep-2024 |
Fakultät: | SE - Sonstige Einrichtungen |
Fachrichtung: | SE - DFKI Deutsches Forschungszentrum für Künstliche Intelligenz |
Professur: | SE - Sonstige |
Sammlung: | SciDok - Der Wissenschaftsserver der Universität des Saarlandes |
Dateien zu diesem Datensatz:
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
SEKI-Working-Paper-SWP-89-01_Crone=Rawe_Unification-Algorithms-for-Boolean-Rings.pdf | 87,35 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.