HORPO with Computability Closure : A Reconstruction

Simple item page
dc.creatorBlanqui, Frédéric
dc.creatorJouannaud, Jean-Pierre
dc.creatorRubio, Albert
dc.date2007-08-27
dc.date.accessioned2026-07-07T08:25:51Z
dc.date.available2026-07-07T08:25:51Z
dc.descriptionThis 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.
dc.identifierhttps://arxiv.org/abs/0708.3582
dc.identifierhttp://arxiv.org/abs/0708.3582
dc.identifierDans 14th International Conference on Logic for Programming Artificial Intelligence and Reasoning LNCS (2007)
dc.identifier.urihttp://salesiana.dossiersoluciones.com/handle/123456789/136759
dc.subjectLogic in Computer Science
dc.titleHORPO with Computability Closure : A Reconstruction
dc.typetext

Files

Collections

arXiv