HORPO with Computability Closure : A Reconstruction

Frédéric Blanqui 1 Jean-Pierre Jouannaud 2 Albert Rubio 3
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 LSI - Llenguatges i Sistemes Informàtics
Abstract : This paper provides a new, decidable definition of the higher- order recursive path ordering in which type comparisons are made only when needed, therefore eliminating the need for the computability clo- sure, and bound variables are handled explicitly, making it possible to handle recursors for arbitrary strictly positive inductive types.
keyword : lambda-calculus termination rewriting
Type de document :
Communication dans un congrès
14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Oct 2007, Yerevan, Armenia. 4790, LNCS
Liste complète des métadonnées

Littérature citée [6 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00168304
Contributeur : Frédéric Blanqui <>
Soumis le : lundi 27 août 2007 - 12:21:26
Dernière modification le : mercredi 25 avril 2018 - 10:45:20
Document(s) archivé(s) le : vendredi 9 avril 2010 - 01:10:38

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00168304, version 1
  • ARXIV : 0708.3582

Collections

INRIA | LIX | X-LIX | X | PARISTECH | LORIA | UNIV-LORRAINE

Citation

Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio. HORPO with Computability Closure : A Reconstruction. 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Oct 2007, Yerevan, Armenia. 4790, LNCS. 〈inria-00168304〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

212

Téléchargements de fichiers

238

Contact


archive-ouverte@inria.fr