Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
Summary :
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.
- Publication
- IEICE TRANSACTIONS on Information Vol.E88-D No.12 pp.2715-2726
- Publication Date
- 2005/12/01
- Publicized
- Online ISSN
- DOI
- 10.1093/ietisy/e88-d.12.2715
- Type of Manuscript
- PAPER
- Category
- Computation and Computational Models
Authors
Keyword
Latest Issue
Copyrights notice of machine-translated contents
The copyright of the original papers published on this site belongs to IEICE. Unauthorized use of the original or translated papers is prohibited. See IEICE Provisions on Copyright for details.
Cite this
Copy
Keiichirou KUSAKARI, Masahiko SAKAI, Toshiki SAKABE, "Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting" in IEICE TRANSACTIONS on Information,
vol. E88-D, no. 12, pp. 2715-2726, December 2005, doi: 10.1093/ietisy/e88-d.12.2715.
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.
URL: https://global.ieice.org/en_transactions/information/10.1093/ietisy/e88-d.12.2715/_p
Copy
@ARTICLE{e88-d_12_2715,
author={Keiichirou KUSAKARI, Masahiko SAKAI, Toshiki SAKABE, },
journal={IEICE TRANSACTIONS on Information},
title={Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting},
year={2005},
volume={E88-D},
number={12},
pages={2715-2726},
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.},
keywords={},
doi={10.1093/ietisy/e88-d.12.2715},
ISSN={},
month={December},}
Copy
TY - JOUR
TI - Primitive Inductive Theorems Bridge Implicit Induction Methods and Inductive Theorems in Higher-Order Rewriting
T2 - IEICE TRANSACTIONS on Information
SP - 2715
EP - 2726
AU - Keiichirou KUSAKARI
AU - Masahiko SAKAI
AU - Toshiki SAKABE
PY - 2005
DO - 10.1093/ietisy/e88-d.12.2715
JO - IEICE TRANSACTIONS on Information
SN -
VL - E88-D
IS - 12
JA - IEICE TRANSACTIONS on Information
Y1 - December 2005
AB - 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.
ER -
English
