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

Kentaro Kikuchi, Takahito Aoto, Isao Sasano

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
PublisherAssociation for Computing Machinery
ISBN (Electronic)9781450372497
DOIs
Publication statusPublished - 2019 Oct 7
Event21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019 - Porto, Portugal
Duration: 2019 Oct 72019 Oct 9

Publication series

NameACM International Conference Proceeding Series

Conference

Conference21st International Symposium on Principles and Practice of Declarative Programming, PPDP 2019
CountryPortugal
CityPorto
Period19/10/719/10/9

Keywords

  • Confluence
  • Inductive Theorem Proving
  • Infinite List
  • Non-termination
  • Program Transformation
  • Sufficient Completeness
  • Term Rewriting

ASJC Scopus subject areas

  • Software
  • Human-Computer Interaction
  • Computer Vision and Pattern Recognition
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Inductive theorem proving in non-terminating rewriting systems and its application to program transformation'. Together they form a unique fingerprint.

Cite this