EXPLANATION-BASED LEARNING AND REFORMATION FOR PROGRAM GENERATION,TRANSFORMATION,AND VERIFICATION

本研究旨在为软件科学中最活跃的研究领域之一--程序生成、转换和验证领域的基于推理的学习（EBL）技术奠定基础和应用。研究结果分为五个部分，每个部分对应最后报告的一个章节。前两个结果提供了研究的理论基础，而其他三个分别呈现了关于验证，生成和转换的结果。1.建立了一类方程语言的元工具。这保证了EBL机制可以被纳入语言的反射框架。2.研究了等式语言框架中的模块性。特别地，形式化地证明了在验证和生成中起重要作用的简单终止性的模块性。3.将EBL应用于项重写系统的终止性验证。该技术成功地提高了整个系统的效率。4.将EBL应用于基于Kunth-Benzetron完成的项重写系统的程序生成。该技术使我们能够开发出一个有效的程序完成多个减少订单。5.保持终止的程序转换技术已被研究，并应用于分析的组合项重写系统。EBL与推广已知的转换技术的过程有关。

This research aims at developing foundations and applications of explanation-based learning (EBL) techniques for the domain of program generation, transformation, and verification, which is one of the most active area of research field in software science. The results of the research are divided into five parts, each corresponding to a single chapter of the final report. The first two results provide the theoretical foundation of the research, while the other three present the results concerning verification, generation, and transformation, respectively. The are summarizad as follows :1.Meta-facility for a class of equational languages has been developed. This ensures that EBL mechanisms can be incorporated in the reflective framework of the languages.2.Modularity in the framework of equational languages has been studied. In paticular, the modularity of simple termination, which plays an important role in verification and generation, has been formally proved.3.The EBL has been applied to the verification of termination of term rewriting systems. The technique has successfully improved the efficiency of the overall system.4.The EBL has been applied to the program generation based on Kunth-Bendix completion of term rewriting systems. The technique has allowed us to develop an efficient procedure for completion with multiple reduction orderings.5.A program tarnsformation technique which preserves termination has been studied and applied to the analysis of composable combination of term rewriting systems. The EBL is related to the process of generalizing known techniques of tranformation.