Decidability of Inductive Theorems based on Rewriting Induction

DOI

Bibliographic Information

Other Title
  • 書き換え帰納法に基づく帰納的定理の決定可能性

Description

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 validity, 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.

Journal

  • Computer Software

    Computer Software 31 (3), 3_294-3_306, 2014

    Japan Society for Software Science and Technology

Related Projects

See more

Details 詳細情報について

  • CRID
    1390001204738467200
  • NII Article ID
    130004688287
  • DOI
    10.11309/jssst.31.3_294
  • ISSN
    02896540
  • Text Lang
    ja
  • Article Type
    journal article
  • Data Source
    • JaLC
    • CiNii Articles
    • KAKEN
  • Abstract License Flag
    Disallowed

Report a problem

Back to top