Please login using the form on menu list.|
It is required to login for Full-Text PDF.
Mechanizing Explicit Inductive Equational Reasoning by DTRC
IEICE TRANSACTIONS on Information and Systems Vol.E78-D No.2 pp.113-121
Publication Date: 1995/02/20
Print ISSN: 0916-8532
Type of Manuscript: PAPER
Category: Algorithm and Computational Complexity
inductive equational reasoning,
cover set induction,
term rewriting systems,
dynamic term rewriting calculus,
Full Text: PDF
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.