Decidability of inductive theorems based on rewriting induction

Tatsunari Nakazima, Takahito Aoto, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

1 Citation (Scopus)


In equational logics, validity of equations on data structures such as natural numbers or lists is formalized as inductive validity; and the equations inductively valid are called inductive theorems. In general, it is undecidable whether an equation is an inductive theorem of an equational logic. Thus, several decision procedures of inductive validity for some subclasses of conjectures have been known. A decision procedure given by Falke and Kapur (2006) is based on rewriting induction. Toyama (2002) gives a sufficient criterion of conjectures for which the rewriting induction procedure becomes a decision procedure for inductive va- lidity, by reducing the problem of inductive validity to a problem of equivalence of two abstract reduction systems. However, the classes of conjectures having decidable inductive validity obtained by Falke and Kapur and obtained by Toyama are incomparable. In this paper, we extend known classes of conjectures having decidable inductive validity, combining these two approaches.

Original languageEnglish
Pages (from-to)294-306
Number of pages13
JournalComputer Software
Issue number3
Publication statusPublished - 2014 Aug 1

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'Decidability of inductive theorems based on rewriting induction'. Together they form a unique fingerprint.

Cite this