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).
Chengcheng JI
Hokkaido University
Masahito KURIHARA
Hokkaido University
Haruhiko SATO
Hokkai-Gakuen University
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Copy
Chengcheng JI, Masahito KURIHARA, Haruhiko SATO, "Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection" in IEICE TRANSACTIONS on Information,
vol. E102-D, no. 2, pp. 223-238, February 2019, doi: 10.1587/transinf.2017EDP7368.
Abstract: 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).
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.2017EDP7368/_p
Copy
@ARTICLE{e102-d_2_223,
author={Chengcheng JI, Masahito KURIHARA, Haruhiko SATO, },
journal={IEICE TRANSACTIONS on Information},
title={Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection},
year={2019},
volume={E102-D},
number={2},
pages={223-238},
abstract={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).},
keywords={},
doi={10.1587/transinf.2017EDP7368},
ISSN={1745-1361},
month={February},}
Copy
TY - JOUR
TI - Multi-Context Automated Lemma Generation for Term Rewriting Induction with Divergence Detection
T2 - IEICE TRANSACTIONS on Information
SP - 223
EP - 238
AU - Chengcheng JI
AU - Masahito KURIHARA
AU - Haruhiko SATO
PY - 2019
DO - 10.1587/transinf.2017EDP7368
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E102-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 2019
AB - 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).
ER -