Paper Info
Title
Inductive Theorems for Higher-Order Rewriting
Abstract
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.
Year
DOI
Venue
2004
10.1007/978-3-540-25979-4_19
Lecture Notes in Computer Science
Keywords
Field
DocType
inductive reasoning,first order,higher order
Inductive reasoning,Discrete mathematics,Computer science,Algorithm,Decidability,Rewriting,Confluence,Completeness (statistics)
Conference
Volume
ISSN
Citations 
3091
0302-9743
4
PageRank 
References 
Authors
0.45
14
3
Name
Order
Citations
PageRank
Takahito Aoto112117.53
Toshiyuki Yamada2403.59
Yoshihito Toyama353349.60