Inductive theorem proving in non-terminating rewriting systems and its application to program transformation

Kentaro Kikuchi, Takahito Aoto, Isao Sasano

研究成果: Conference contribution

2 被引用数 (Scopus)

抄録

We present a framework for proving inductive theorems of first-order equational theories, using techniques of implicit induction developed in the field of term rewriting. In this framework, we make use of automated confluence provers, which have recently been developed intensively, as well as a novel condition of sufficient completeness, called local sufficient completeness. The condition is a key to automated proof of inductive theorems of term rewriting systems that include non-terminating functions. We also apply the technique to showing the correctness of program transformation that is realised as an equivalence transformation of term rewriting systems.

本文言語English
ホスト出版物のタイトルProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
出版社Association for Computing Machinery
ISBN(電子版)9781450372497
DOI
出版ステータスPublished - 2019 10 7
イベント21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019 - Porto, Portugal
継続期間: 2019 10 72019 10 9

出版物シリーズ

名前ACM International Conference Proceeding Series

Conference

Conference21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
国/地域Portugal
CityPorto
Period19/10/719/10/9

ASJC Scopus subject areas

  • ソフトウェア
  • 人間とコンピュータの相互作用
  • コンピュータ ビジョンおよびパターン認識
  • コンピュータ ネットワークおよび通信

フィンガープリント

「Inductive theorem proving in non-terminating rewriting systems and its application to program transformation」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル