For Full-Text PDF, please login, if you are a member of IEICE,|
or go to Pay Per View on menu list, if you are a nonmember of IEICE.
Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection
Chengcheng JI Masahito KURIHARA Haruhiko SATO
IEICE TRANSACTIONS on Information and Systems
Publication Date: 2019/02/01
Online ISSN: 1745-1361
Type of Manuscript: PAPER
Category: Fundamentals of Information Systems
term rewriting systems, term rewriting induction, multi-context induction, lemma generation,
Full Text: PDF(367.2KB)
>>Buy this Article
We present an automated lemma generation method for equational, inductive theorem proving based on the term rewriting induction of Reddy and Aoto as well as the divergence critic framework of Walsh. The method effectively works by using the divergence-detection technique to locate differences in diverging sequences, and generates potential lemmas automatically by analyzing these differences. We have incorporated this method in the multi-context inductive theorem prover of Sato and Kurihara to overcome the strategic problems resulting from the unsoundness of the method. The experimental results show that our method is effective especially for some problems diverging with complex differences (i.e., parallel and nested differences).