Mechanizing Explicit Inductive Equational Reasoning by DTRC
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E78-D No.2 pp.113-121
- Publication Date
- 1995/02/25
- Publicized
- Online ISSN
- DOI
- Type of Manuscript
- PAPER
- Category
- Algorithm and Computational Complexity
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
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.
Cite this
Copy
Su FENG, Toshiki SAKABE, Yasuyoshi INAGAKI, "Mechanizing Explicit Inductive Equational Reasoning by DTRC" in IEICE TRANSACTIONS on Information,
vol. E78-D, no. 2, pp. 113-121, February 1995, doi: .
Abstract: 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.
URL: https://global.ieice.org/en_transactions/information/10.1587/e78-d_2_113/_p
Copy
@ARTICLE{e78-d_2_113,
author={Su FENG, Toshiki SAKABE, Yasuyoshi INAGAKI, },
journal={IEICE TRANSACTIONS on Information},
title={Mechanizing Explicit Inductive Equational Reasoning by DTRC},
year={1995},
volume={E78-D},
number={2},
pages={113-121},
abstract={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.},
keywords={},
doi={},
ISSN={},
month={February},}
Copy
TY - JOUR
TI - Mechanizing Explicit Inductive Equational Reasoning by DTRC
T2 - IEICE TRANSACTIONS on Information
SP - 113
EP - 121
AU - Su FENG
AU - Toshiki SAKABE
AU - Yasuyoshi INAGAKI
PY - 1995
DO -
JO - IEICE TRANSACTIONS on Information
SN -
VL - E78-D
IS - 2
JA - IEICE TRANSACTIONS on Information
Y1 - February 1995
AB - 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.
ER -
English
