Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
Inductive Theorem Proving in Non-terminating Rewriting Systems and Its Application to Program Transformation
复制标题
非终止重写系统中的归纳定理证明及其在程序转换中的应用
DOI：
10.1145/3354166.3354178
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Isao Sasano
中科院分区：
文献类型：
--
作者：
Kentaro Kikuchi;Takahito Aoto;Isao Sasano
我们提出了一个框架来证明一阶方程理论的归纳定理，使用隐式归纳法在项重写领域发展起来的技术。在这个框架中，我们使用了最近被大量开发的自动合流证明器，以及一个新的充分完备性条件，称为局部充分完备性。该条件是包含非终止函数的项改写系统的归纳定理自动证明的关键。我们还应用该技术来证明程序转换的正确性，该转换是作为项重写系统的等价转换实现的。
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.