TY - GEN
T1 - Inductive theorem proving in non-terminating rewriting systems and its application to program transformation
AU - Kikuchi, Kentaro
AU - Aoto, Takahito
AU - Sasano, Isao
N1 - Funding Information:
We are grateful to the anonymous referees for valuable comments. The first author thanks the Japan Society for the Promotion of Science (JSPS), Core-to-Core Program (A. Advanced Research Networks) for supporting this research. The research was also supported by JSPS KAKENHI Grant Numbers 17K00005, 18K11158 and 19K11891.
Publisher Copyright:
© 2019 ACM.
PY - 2019/10/7
Y1 - 2019/10/7
N2 - We present a framework for proving inductive theorems of first-order equational theories, using techniques of implicit induction developed in the field of term rewriting. In this framework, we make use of automated confluence provers, which have recently been developed intensively, as well as a novel condition of sufficient completeness, called local sufficient completeness. The condition is a key to automated proof of inductive theorems of term rewriting systems that include non-terminating functions. We also apply the technique to showing the correctness of program transformation that is realised as an equivalence transformation of term rewriting systems.
AB - We present a framework for proving inductive theorems of first-order equational theories, using techniques of implicit induction developed in the field of term rewriting. In this framework, we make use of automated confluence provers, which have recently been developed intensively, as well as a novel condition of sufficient completeness, called local sufficient completeness. The condition is a key to automated proof of inductive theorems of term rewriting systems that include non-terminating functions. We also apply the technique to showing the correctness of program transformation that is realised as an equivalence transformation of term rewriting systems.
KW - Confluence
KW - Inductive Theorem Proving
KW - Infinite List
KW - Non-termination
KW - Program Transformation
KW - Sufficient Completeness
KW - Term Rewriting
UR - http://www.scopus.com/inward/record.url?scp=85083364019&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85083364019&partnerID=8YFLogxK
U2 - 10.1145/3354166.3354178
DO - 10.1145/3354166.3354178
M3 - Conference contribution
AN - SCOPUS:85083364019
T3 - ACM International Conference Proceeding Series
BT - Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
PB - Association for Computing Machinery
T2 - 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
Y2 - 7 October 2019 through 9 October 2019
ER -