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
귀납적 정리 증명은 시스템의 형식적 검증 분야에서 중요한 역할을 합니다. Rewriting Induction(RI)은 Reddy가 제안한 귀납적 정리 증명 방법입니다. 성공적인 증명을 얻으려면 RI 추론 규칙을 적용할 때 적절한 컨텍스트(각 방정식이 어느 방향으로 향해야 하는지 등)를 선택하는 것이 매우 중요합니다. 선택이 적절하지 않은 경우 절차가 다양해지거나 사용자는 기본 정리와 함께 증명하기 위해 여러 보조정리를 생각해내야 합니다. 따라서 우리는 성공적인 증명을 찾기 위해 각각 구별된 단일 컨텍스트를 담당하는 재작성 유도 절차의 여러 인스턴스의 병렬 실행을 고려할 충분한 이유가 있습니다. 본 논문에서는 다음과 같은 새로운 절차를 제안한다. 다중 상황 재작성 유도, 이는 다음과 같은 아이디어를 기반으로 단일 프로세스에서 재작성 유도 절차의 병렬 실행을 효율적으로 시뮬레이션합니다. 다중 완료 절차. 잘 알려진 문제 세트에 대한 실험을 통해 성공적인 귀납적 증명을 위해 다양한 상황을 검색할 때 제안된 절차의 효율성을 논의합니다.
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.
부
Haruhiko SATO, Masahito KURIHARA, "Multi-Context Rewriting Induction with Termination Checkers" in IEICE TRANSACTIONS on Information,
vol. E93-D, no. 5, pp. 942-952, May 2010, doi: 10.1587/transinf.E93.D.942.
Abstract: Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.
URL: https://global.ieice.org/en_transactions/information/10.1587/transinf.E93.D.942/_p
부
@ARTICLE{e93-d_5_942,
author={Haruhiko SATO, Masahito KURIHARA, },
journal={IEICE TRANSACTIONS on Information},
title={Multi-Context Rewriting Induction with Termination Checkers},
year={2010},
volume={E93-D},
number={5},
pages={942-952},
abstract={Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.},
keywords={},
doi={10.1587/transinf.E93.D.942},
ISSN={1745-1361},
month={May},}
부
TY - JOUR
TI - Multi-Context Rewriting Induction with Termination Checkers
T2 - IEICE TRANSACTIONS on Information
SP - 942
EP - 952
AU - Haruhiko SATO
AU - Masahito KURIHARA
PY - 2010
DO - 10.1587/transinf.E93.D.942
JO - IEICE TRANSACTIONS on Information
SN - 1745-1361
VL - E93-D
IS - 5
JA - IEICE TRANSACTIONS on Information
Y1 - May 2010
AB - Inductive theorem proving plays an important role in the field of formal verification of systems. The rewriting induction (RI) is a method for inductive theorem proving proposed by Reddy. In order to obtain successful proofs, it is very important to choose appropriate contexts (such as in which direction each equation should be oriented) when applying RI inference rules. If the choice is not appropriate, the procedure may diverge or the users have to come up with several lemmas to prove together with the main theorem. Therefore we have a good reason to consider parallel execution of several instances of the rewriting induction procedure, each in charge of a distinguished single context in search of a successful proof. In this paper, we propose a new procedure, called multi-context rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multi-completion procedure. By the experiments with a well-known problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.
ER -