Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-39777
Titel: | Completion of Globally Finite Term Rewriting Systems for Inductive Proofs |
VerfasserIn: | Göbel, Richard |
Sprache: | Englisch |
Erscheinungsjahr: | 1986 |
Erscheinungsort: | Kaiserslautern |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | The Knuth-Bendix Algorithm (KBA) is not able to complete term rewriting systems with cyclic rules such as the commutativity. This kind of rules cause cycles in a reduction chain. This problem may be solved by an extension of the KBA for globally finite term rewriting systems. For a globally finite term rewriting system, cycles may occur in a reduction chain, but for each term there is only a finite set of reductions. A confluent and globally finite term rewriting system R provides a decision procedure for equality induced by R: Two terms are equal iff there is a common term in their reduction sets. This extension requires new methods for testing the global finiteness and a new confluence test, because local confluence does not imply global confluence for globally finite relations. In this paper we give a theoretical framework for this extension. We will show how this theory can be applied to term rewriting systems, if we are mainly interested in the initial algebra which is induced by the set of rules. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-397779 hdl:20.500.11880/37669 http://dx.doi.org/10.22028/D291-39777 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 86,6 |
Datum des Eintrags: | 21-Mai-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-REPORT-SR-86-06_Göbel_Completion-of-Globally-Finite-Term-Rewriting-Systems-for-Inductive-Proofs.pdf | 9,81 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.