The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. ex. Some numerals are expressed as "XNUMX".
Copyrights notice
The original paper is in English. Non-English content has been machine-translated and may contain typographical errors or mistranslations. Copyrights notice
우리는 Reddy와 Aoto의 용어 재작성 유도와 Walsh의 발산 비평 프레임워크를 기반으로 방정식, 귀납적 정리 증명을 위한 자동화된 보조정리 생성 방법을 제시합니다. 이 방법은 발산 탐지 기술을 사용하여 발산 시퀀스의 차이점을 찾아 효과적으로 작동하고 이러한 차이점을 분석하여 잠재적인 보조정리를 자동으로 생성합니다. 우리는 이 방법의 불건전함으로 인한 전략적 문제를 극복하기 위해 Sato와 Kurihara의 다중 상황 귀납 정리 증명에 이 방법을 통합했습니다. 실험 결과는 우리의 방법이 특히 복잡한 차이로 분기되는 일부 문제(예: 병렬 및 중첩 차이)에 효과적이라는 것을 보여줍니다.
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.
부
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
부
@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},}
부
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 -