A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
In: Theoretical Aspects of Computing – ICTAC 2021 ISBN: 9783030853143 ICTAC; (2021)
Online
unknown
Zugriff:
A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. In this paper, we present a proof method for local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness and is useful for proving inductive theorems of non-terminating TRSs. The proof method is based on a sufficient condition for local sufficient completeness of TRSs that consist of functions on natural numbers and (possibly infinite) lists of natural numbers. We also make a comparison between the proof abilities of the methods by the sufficient condition and by a derivation system introduced in previous work.
Titel: |
A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
|
---|---|
Autor/in / Beteiligte Person: | Kikuchi, Kentaro ; Shiraishi, Tomoki ; Aoto, Takahito |
Link: | |
Quelle: | Theoretical Aspects of Computing – ICTAC 2021 ISBN: 9783030853143 ICTAC; (2021) |
Veröffentlichung: | Springer International Publishing, 2021 |
Medientyp: | unknown |
ISBN: | 978-3-030-85314-3 (print) |
DOI: | 10.1007/978-3-030-85315-0_22 |
Schlagwort: |
|
Sonstiges: |
|