Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-40371
Titel: | Path and decomposition orderings for proving AC-termination |
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 Lexicographical ordering Multiset ordering Path of subterms ordering Recursive decomposition ordering Recursive path ordering Simplification ordering Status Termination Term rewriting system Well-founded ordering |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | Term rewriting provides a simple mechanism that can be applied to reasoning in structures defined by 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. An appropriate reduction relation allows reductions modulo the equations in E. The effective computation with this relation presumes E-termination. We will give an overview and a classification of the well-known methods guaranteeing AC-termination based on the recursive path ordering. Furthermore, we will show that these techniques [called associative path orderings] cannot use quasi-orderings on operators. Above all, this report will deal with some new orderings applicable to AC-theories. We apply a slight extension [the embedding of status] of the concept of the associative path ordering of Gnaedig and Lescanne to several path and decomposition orderings. Since these orderings are stronger than the recursive path ordering, the corresponding orderings restricted to AC-theories are more powerful than the associative path ordering. From a practical point of view these new AC-orderings are more interesting than the associative path ordering because the automatic detection of an admissible precedence for orienting the rules of a given system is much easier. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-403713 hdl:20.500.11880/37706 http://dx.doi.org/10.22028/D291-40371 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 89,18 |
Datum des Eintrags: | 24-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-89-18_Steinbach_Path-and-decomposition-orderings-for-proving-AC=termination.pdf | 57,33 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.