季承成 | CHENGCHENG JI
计算机科学与信息技术 博士 | Ph.D. in Computer Science and Information Technology
Automated Proof and Discovery of Inductive Theorems with Rewriting Induction over Multi-Context Reasoning Systems: State-of-the-Art Technologies and Perspectives
摘要/ABSTRACT
A system for efficiently running mutually related virtual processes as a single process is called a multi-context reasoning system. We focus on its application to automated proof and discovery of inductive theorems in the framework of rewriting induction and briefly survey past and current state-of-the-art technologies of such systems. Then to deal with lemma discovery in this framework, we present an extension of MRIt, the multi-context rewriting induction system with termination tools developed by Sato and Kurihara, and discuss its effectiveness.
作者/Authors
Masahito Kurihara, Haruhiko Sato, ChengCheng Ji
会议信息/Information
Lecture Notes in Engineering and Computer Science: Proc. of The World Congress on Engineering and Computer Science 2018, San Francisco, USA, pp. 149-154 (EI).