Mechanizing Explicit Inductive Equational Reasoning by DTRC

Su FENG  Toshiki SAKABE  Yasuyoshi INAGAKI 

Publication
IEICE TRANSACTIONS on Information and Systems  Vol.E78-D  No.2  pp.113-121
Publication Date: 1995/02/20
Online ISSN: 
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Algorithm and Computational Complexity
Keyword: 
inductive equational reasoning,  structural induction,  cover set induction,  term rewriting systems,  dynamic term rewriting calculus, 

Full Text: PDF

Summary: 
Dynamic Term Rewriting Calculus (DTRC) is a new computation model aiming at formal description and verification of algorithms treating Term Rewriting Systems (TRSs). In this paper, we show that we can use DTRC to mechanize explicit induction for proving an inductive theorem, that is, we can translate the statements of base and induction steps for proving by induction into a DTRC term. The translation reduces the proof of the statements into the evaluation of the corresponding DTRC term.