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ößeFormat 
SEKI-Working-Paper-SWP-89-01_Crone=Rawe_Unification-Algorithms-for-Boolean-Rings.pdf87,35 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.