
For FullText PDF, please login, if you are a member of IEICE,
or go to Pay Per View on menu list, if you are a nonmember of IEICE.

MultiContext Rewriting Induction with Termination Checkers
Haruhiko SATO Masahito KURIHARA
Publication
IEICE TRANSACTIONS on Information and Systems
Vol.E93D
No.5
pp.942952 Publication Date: 2010/05/01
Online ISSN: 17451361
DOI: 10.1587/transinf.E93.D.942
Print ISSN: 09168532 Type of Manuscript: Special Section PAPER (Special Section on Formal Approach) Category: Term Rewriting Systems Keyword: equational theorem proving, term rewriting systems, mathematical induction, rewriting induction, multicompletion,
Full Text: PDF(581.4KB)>>
Summary:
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 multicontext rewriting induction, which efficiently simulates parallel execution of rewriting induction procedures in a single process, based on the idea of the multicompletion procedure. By the experiments with a wellknown problem set, we discuss the effectiveness of the proposed procedure when searching along various contexts for a successful inductive proof.

