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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-93-19_Sattler=Klein_About-Changing-the-Ordering-During-Knuth=Bendix-Completion .pdf | 1,96 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.