Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-38731
Titel: A Completion Procedure for Globally Finite Term Rewriting Systems
VerfasserIn: Göbel, Richard
Sprache: Englisch
Erscheinungsjahr: 1983
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: The Knuth-Bendix Algorithm is not able to complete term rewriting systems (TRS) with cyclic rules such as commutativity, associativity etc. A solution for this problem is to separate the cyclic rules from the TRS and incorporate them into the unification algorithm. This requires a unification algorithm for the specific theory. Usually it is very difficult to develop such algorithms, and we therefore discuss another way to solve this problem. We propose an extension of the completion procedure for globally finite TRS. For a globally finite TRS cycles may occur in a reduction chain, but for each term there is only a finite set of reductions. A confluent and globally finite TRS R provides a decision procedure for the 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 whether a given TRS is confluent and globally finite. For proving that a TRS is globally finite appropriate ordering relations are required, which are usually reflexive. Proving the confluence of a globally finite TRS is more difficult than for nötherian TRS and the set of critical pairs which has to be tested is in general infinite. Therefore a completion procedure with this test may not terminate. Further work has to be done to decrease this critical pair set.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-387313
hdl:20.500.11880/35053
http://dx.doi.org/10.22028/D291-38731
Schriftenreihe: Memo SEKI : SEKI-Projekt / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI
Band: 83,12
Datum des Eintrags: 30-Jan-2023
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-MEMO-83-12_Göbel_A-Completition-Procedure-for-Globally-Finite-Term-Rewriting-Systems.pdf17,53 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.