Inductive theorems for higher-order rewriting

Takahito Aoto, Toshiyuki Yamada, Yoshihito Toyama

Research output: Contribution to journalArticlepeer-review

4 Citations (Scopus)


Based on the simply typed term rewriting framework, inductive reasoning in higher-order rewriting is studied. The notion of higher-order inductive theorems is introduced to reflect higher-order feature of simply typed term rewriting. Then the inductionless induction methods in first-order term rewriting are incorporated to verify higher-order inductive theorems. In order to ensure that higher-order inductive theorems are closed under contexts, the notion of higher-order sufficient completeness is introduced. Finally, the decidability of higher-order sufficient completeness is discussed.

Original languageEnglish
Pages (from-to)269-284
Number of pages16
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publication statusPublished - 2004 Dec 1

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Inductive theorems for higher-order rewriting'. Together they form a unique fingerprint.

Cite this