Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting

Access this Article

Search this Article

Author(s)

Abstract

Automated reasoning of inductive theorems is considered important in program verification. To verify inductive theorems automatically, several implicit induction methods like the inductionless induction and the rewriting induction methods have been proposed. In studying inductive theorems on higher-order rewritings, we found that the class of the theorems shown by known implicit induction methods does not coincide with that of inductive theorems, and the gap between them is a barrier in developing mechanized methods for disproving inductive theorems. This paper fills this gap by introducing the notion of primitive inductive theorems, and clarifying the relation between inductive theorems and primitive inductive theorems. Based on this relation, we achieve mechanized methods for proving and disproving inductive theorems.

Journal

  • IEICE Transactions on Information and Systems

    IEICE Transactions on Information and Systems 88(12), 2715-2726, 2005-12-01

    IEICE

References:  23

Cited by:  6

Codes

  • NII Article ID (NAID)
    110004019494
  • NII NACSIS-CAT ID (NCID)
    AA10826272
  • Text Lang
    ENG
  • Article Type
    Journal Article
  • ISSN
    09168532
  • Data Source
    CJP  CJPref  NII-ELS  IR 
Page Top