TY - GEN
T1 - A Proof Method for Local Sufficient Completeness of Term Rewriting Systems
AU - Shiraishi, Tomoki
AU - Kikuchi, Kentaro
AU - Aoto, Takahito
N1 - Funding Information:
Acknowledgements. We are grateful to the anonymous referees for valuable comments. This work was partly supported by JSPS KAKENHI Grant Numbers JP19K11891, JP20H04164 and JP21K11750.
Publisher Copyright:
© 2021, Springer Nature Switzerland AG.
PY - 2021
Y1 - 2021
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85115190214&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85115190214&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-85315-0_22
DO - 10.1007/978-3-030-85315-0_22
M3 - Conference contribution
AN - SCOPUS:85115190214
SN - 9783030853143
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 386
EP - 404
BT - Theoretical Aspects of Computing – ICTAC 2021 - 18th International Colloquium, Proceedings
A2 - Cerone, Antonio
A2 - Olveczky, Peter Csaba
PB - Springer Science and Business Media Deutschland GmbH
T2 - 18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
Y2 - 8 September 2021 through 10 September 2021
ER -