Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40254
Titel: | Proving termination of associative-commutative rewriting systems using the Knuth-Bendix ordering |
VerfasserIn: | Steinbach, Joachim |
Sprache: | Englisch |
Erscheinungsjahr: | 1989 |
Erscheinungsort: | Kaiserslautern |
Freie Schlagwörter: | Associative and commutative operators Associative path ordering E-commuting E-compatible Equational theories Flattening Knuth-Bendix ordering Lexicographical ordering Multiset ordering Polynomial ordering Recursive path ordering Simplification ordering Status Termination Term rewriting system Well-founded ordering |
DDC-Sachgruppe: | 000 Allgemeines, Wissenschaft |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Term rewriting systems provide a simple mechanism for computing in equations. An equation is converted into a directed rewrite rule by comparing both sides w.r.t. an ordering. However, there exist equations which are incomparable. The handling of such equations includes, for example, partitioning the given equational theory into a set R of rules and a set E of equations. The appropriate reduction relation allows reductions modulo the equations in E. The effective computation with this relation presumes E-termination. Classical termination methods cannot directly guarantee E-termination. This report deals with a new ordering applicable to (R,E)-systems where E contains associative-commutative equations. The method is based on the Knuth-Bendix ordering and is AC-commuting, a property introduced by Jouannaud and Munoz. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-402542 hdl:20.500.11880/36263 http://dx.doi.org/10.22028/D291-40254 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 89,13 |
Datum des Eintrags: | 14-Aug-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öße | Format | |
---|---|---|---|---|
SEKI-Report-SR-89-13_Steinbach_Proving-termination-of-associative=commutative-rewriting-systems-using-the-Knuth=Bendix-ordering.pdf | 7,24 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.