HORPO with Computability Closure : A Reconstruction

Frédéric Blanqui; Jean-Pierre Jouannaud; Albert Rubio

inria-00168304, version 1

HORPO with Computability Closure : A Reconstruction

Frédéric Blanqui ()^a^, 1, Jean-Pierre Jouannaud ()^b^, 2, Albert Rubio ()^c^, 3

14th International Conference on Logic for Programming Artificial Intelligence and Reasoning 4790 (2007)

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.

a – INRIA
b – Polytechnique - X
c – Universitat Politècnica de Catalunya
1: PROTHEO (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
2: Laboratoire d'informatique de l'école polytechnique (LIX)
CNRS : UMR7161 – Polytechnique - X
3: Llenguatges i Sistemes Informàtics (LSI)
Universitat Politécnica de Catalunya

inria-00168304, version 1
http://hal.inria.fr/inria-00168304
oai:hal.inria.fr:inria-00168304
From: Frédéric Blanqui <>
Submitted on: Monday, 27 August 2007 12:21:26
Updated on: Wednesday, 29 August 2007 09:38:25

See detailed view

Associated documents

PS :

PDF :

arXiv: 0708.3582

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00168304"><analytic>
<author><persName><forename>Frédéric</forename><surname>Blanqui</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">PROTHEO</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<author><persName><forename>Jean-Pierre</forename><surname>Jouannaud</surname></persName>
<affiliation>
<orgName type="laboratory">LIX</orgName>
<orgName type="team">Laboratoire d'informatique de l'école polytechnique</orgName>
<country>FR</country>
<orgName type="institution">CNRS : UMR7161</orgName>
<orgName type="institution">Polytechnique - X</orgName>
</affiliation>
</author>
<author><persName><forename>Albert</forename><surname>Rubio</surname></persName>
<affiliation>
<orgName type="laboratory">LSI</orgName>
<orgName type="team">Llenguatges i Sistemes Informàtics</orgName>
<country>ES</country>
<orgName type="institution">Universitat Politécnica de Catalunya</orgName>
</affiliation>
</author>
<title type="main" level="a">HORPO with Computability Closure : A Reconstruction</title></analytic><monogr><meeting>14th International Conference on Logic for Programming Artificial Intelligence and Reasoning</meeting><imprint><pubPlace><settlement>Yerevan</settlement><country>Armenia</country></pubPlace><biblScope type="publicationDate">2007-10-15</biblScope><biblScope type="vol">4790</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/inria-00168304</idno><idno type="HALFile">http://hal.inria.fr/inria-00168304/PDF/main.pdf</idno></biblStruct>
</listBibl>
</listBibl>