The search functionality is under construction.
The search functionality is under construction.

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

Chengcheng JI, Masahito KURIHARA, Haruhiko SATO

  • Full Text Views

    0

  • Cite this

Summary :

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).

Publication
IEICE TRANSACTIONS on Information Vol.E102-D No.2 pp.223-238
Publication Date
2019/02/01
Publicized
2018/11/12
Online ISSN
1745-1361
DOI
10.1587/transinf.2017EDP7368
Type of Manuscript
PAPER
Category
Fundamentals of Information Systems

Authors

Chengcheng JI
  Hokkaido University
Masahito KURIHARA
  Hokkaido University
Haruhiko SATO
  Hokkai-Gakuen University

Keyword