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ößeFormat 
SEKI-Report-SR-89-18_Steinbach_Path-and-decomposition-orderings-for-proving-AC=termination.pdf57,33 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.