Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection

Chengcheng JI  Masahito KURIHARA  Haruhiko SATO  

IEICE TRANSACTIONS on Information and Systems   Vol.E102-D   No.2   pp.223-238
Publication Date: 2019/02/01
Online ISSN: 1745-1361
DOI: 10.1587/transinf.2017EDP7368
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).