Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-41416
Titel: About Changing the Ordering During Knuth-Bendix Completion
VerfasserIn: Sattler-Klein, Andrea
Sprache: Englisch
Erscheinungsjahr: 1993
Erscheinungsort: Kaiserslautern
DDC-Sachgruppe: 004 Informatik
Dokumenttyp: Forschungsbericht (Report zu Forschungsprojekten)
Abstract: We will answer a question posed in [DJK91], and will show that Huet’s completion algorithm [Hu81] becomes incomplete, i.e. it may generate a term rewriting system that is not confluent, if it is modified in a way that the reduction ordering used for completion can be changed during completion provided that the new ordering is compatible with the actual rules. In particular, we will show that this problem may not only arise if the modified completion algorithm does not terminate: Even if the algorithm terminates without failure, the generated finite noetherian term rewriting system may be non-confluent. Most existing implementations of the Knuth-Bendix algorithm provide the user with help in choosing a reduction ordering: If an unorientable equation is encountered, then the user has many options, especially, the one to orient the equation manually. The integration of this feature is based on the widespread assumption that, if equations are oriented by hand during completion and the completion process terminates with success, then the generated finite system is a maybe nonterminating but locally confluent system (see e.g. [KZ89]). Our examples will show that this assumption is not true.
Link zu diesem Datensatz: urn:nbn:de:bsz:291--ds-414169
hdl:20.500.11880/37714
http://dx.doi.org/10.22028/D291-41416
Schriftenreihe: SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447]
Band: 93,19
Datum des Eintrags: 27-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ößeFormat 
SEKI-Report-SR-93-19_Sattler=Klein_About-Changing-the-Ordering-During-Knuth=Bendix-Completion .pdf1,96 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.