A Proof Method for Local Sufficient Completeness of Term Rewriting Systems

Tomoki Shiraishi, Kentaro Kikuchi, Takahito Aoto

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

Abstract

A term rewriting system (TRS) is said to be sufficiently complete when each function yields some value for any input. In this paper, we present a proof method for local sufficient completeness of TRSs, which is a generalised notion of sufficient completeness and is useful for proving inductive theorems of non-terminating TRSs. The proof method is based on a sufficient condition for local sufficient completeness of TRSs that consist of functions on natural numbers and (possibly infinite) lists of natural numbers. We also make a comparison between the proof abilities of the methods by the sufficient condition and by a derivation system introduced in previous work.

Original languageEnglish
Title of host publicationTheoretical Aspects of Computing – ICTAC 2021 - 18th International Colloquium, Proceedings
EditorsAntonio Cerone, Peter Csaba Olveczky
PublisherSpringer Science and Business Media Deutschland GmbH
Pages386-404
Number of pages19
ISBN (Print)9783030853143
DOIs
Publication statusPublished - 2021
Event18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021 - Virtual, Online
Duration: 2021 Sep 82021 Sep 10

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12819 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference18th International Colloquium on Theoretical Aspects of Computing, ICTAC 2021
CityVirtual, Online
Period21/9/821/9/10

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A Proof Method for Local Sufficient Completeness of Term Rewriting Systems'. Together they form a unique fingerprint.

Cite this