Result: Inductive theorems for higher-order rewriting
Title:
Inductive theorems for higher-order rewriting
Authors:
Source:
RTA 2004 : rewriting techniques and applications (Aachen, 3-5 June 2004)Lecture notes in computer science. :269-284
Publisher Information:
Berlin: Springer, 2004.
Publication Year:
2004
Physical Description:
print, 21 ref
Original Material:
INIST-CNRS
Subject Terms:
Computer science, Informatique, Sciences exactes et technologie, Exact sciences and technology, Sciences appliquees, Applied sciences, Informatique; automatique theorique; systemes, Computer science; control theory; systems, Informatique théorique, Theoretical computing, Théorie programmation, Programming theory, Apprentissage inductif, Inductive learning, Aprendizaje por inducción, Assertion inductive, Inductive assertion, Aserción inductiva, Complétude, Completeness, Completitud, Décidabilité, Decidability, Decidibilidad, Méthode induction, Induction method, Método inducción, Réécriture, Rewriting, Reescritura, Système réécriture, Rewriting systems
Document Type:
Conference
Conference Paper
File Description:
text
Language:
English
Author Affiliations:
Research Institute of Electrical Communication, Tohoku University, Japan
Faculty of Engineering, Mie University, Japan
Faculty of Engineering, Mie University, Japan
ISSN:
0302-9743
Rights:
Copyright 2004 INIST-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
CC BY 4.0
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Notes:
Computer science; theoretical automation; systems
Accession Number:
edscal.15851916
Database:
PASCAL Archive
Further Information
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.