Mechanizing Explicit Inductive Equational Reasoning by DTRC

スポンサーリンク

概要

• 論文の詳細を見る

• 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.

• 社団法人電子情報通信学会の論文
• 1995-02-25

著者

• SAKABE Toshiki

  Department of Information Engineering, Nagoya University

• Sakabe T

  Nagoya Univ. Nagoya Jpn

• INAGAKI Yasuyoshi

  Faculty of Information Science and Technology, Aichi Prefectural University

• Inagaki Y

  Faculty Of Information Science And Technology Aichi Prefectural University

• FENG Su

  Faculty of Engineering, Nagoya University

• Feng Su

  Faculty Of Engineering Nagoya University

関連論文

• An Extension of the Dependency Pair Method for Proving Termination of Higher-Order Rewrite Systems
• Robust Dependency Parsing of Spontaneous Japanese Spoken Language(Speech Corpora and Related Topics, Corpus-Based Speech Technologies)
• Example-Based Query Generation for Spontaneous Speech
• Incremental Transfer in English-Japanese Machine Translation
• A Context Model Approach to Anaphora Resolution in Database-Oriented Discouse
• Confluence Property of Simple Frames in Dynamic Term Rewriting Calculus
• Mechanizing Explicit Inductive Equational Reasoning by DTRC

スポンサーリンク