Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen:
doi:10.22028/D291-41404
Titel: | New Abstract Criteria for Termination and Confluence of Conditional Rewrite Systems |
VerfasserIn: | Gramlich, Bernhard |
Sprache: | Englisch |
Erscheinungsjahr: | 1993 |
Erscheinungsort: | Kaiserslautern |
Freie Schlagwörter: | conditional term rewriting systems overlay systems confluence termination weak termination innermost termination |
DDC-Sachgruppe: | 004 Informatik |
Dokumenttyp: | Forschungsbericht (Report zu Forschungsprojekten) |
Abstract: | We consider the problem of verifying confluence and termination of conditional term rewriting systems (TRSs). For unconditional TRSs the critical pair lemma holds which enables a finite test for confluence of (finite) terminating systems. And for ensuring termination of unconditional TRSs a couple of methods for constructing appropiate well-founded term orderings are known. If however termination is not guaranteed then proving confluence is much more difficult. Recently we have obtained some interesting results for unconditional TRSs which provide sufficient criteria for termination plus confluence in terms of restricted termination and confluence properties. In particular, we have shown that any innermost terminating and locally confluent overlay system is complete, i.e. terminating and confluent. Here we generalize our approach to the conditional case and show how to solve the additional complications due to the presence of conditions in the rules. Our main result can be stated as follows: Any conditional TRS which is an innermost terminating semantical overlay system such that all (conditional) critical pairs are joinable is complete. |
Link zu diesem Datensatz: | urn:nbn:de:bsz:291--ds-414042 hdl:20.500.11880/37713 http://dx.doi.org/10.22028/D291-41404 |
Schriftenreihe: | SEKI-Report / Deutsches Forschungszentrum für Künstliche Intelligenz, DFKI [ISSN 1437-4447] |
Band: | 93,17 |
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-17_Gramlich_New-Abstract-Criteria-for-Termination-and-Confluence-of-Conditional-Rewrite-Systems .pdf | 1,84 MB | Adobe PDF | Öffnen/Anzeigen |
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.