Bienvenido Invitado!

Búsqueda Rápida:  

Búsqueda Avanzada

Idiomas: English Español

Valid XHTML 1.0 Transitional ¡CSS Válido! Icono de conformidad con el Nivel Doble-A, 
	de las Directrices de Accesibilidad para el 
	Contenido Web 1.0 del W3C-WAI

On Some Variants of Second-Order Unification


On Some Variants of Second-Order Unification
On Some Variants of Second-Order Unification

Mateu Villaret i Auselle

Filiación: Universitat de Girona. Departament d'Informática i Matemática Aplicada (Girona, España)

Biografía: No disponible

Cerrar ventana

Mateu Villaret i Auselle

Acerca de los autores 

Año de publicación: 2005

Idioma: inglés

Materias: Ciencia y Tecnología

Colección: Monografies de l'Institut d'Investigació en Intel-ligencia Artificial

eBook gratuito

Resumen:

In this thesis we present several results about Second-Order Unification. It is well known that the Second-Order Unification Problem is in general undecidable; the frontier between its decidable and undecidable subclasses is thin and it still has not been completely defined. Our purpose is to shed some light on the Second-Order Unification problem and study some of its variants. We have mainly focused our attention on Context Unification and Linear Second-Order Unification. Roughly speaking, these problems are variants of Second-Order Unification where second-order variables are required to be linear. Context Unification was defined more than ten years ago and its decidability has been an open question since then. Here we make relevant contributions to the study of this question. The first result that we present is a simplification on these problems thanks to "curryfication". We show that the Context Unification problem can be NP-reduced to the Context Unification problem where, apart from variables, just a single binary function symbol, and first-order constants, are used. We also show that a similar result also holds for Second-Order Unification. The main result of this thesis is the definition of a non-trivial sufficient and necessary condition on the unifiers, for the decidability of Context Unification. The condition is called rank-bound conjecture in order to enforce our belief about its truthness. It lies on a non-trivial measure of terms, the rank, and claims that, whenever an instance of the Context Unification problem is satisfiable, there exists a unifier with a rank not exceeding a certain bound depending on the size of the problem. Under the assumption of this conjecture, we give a reduction of the satisfiability problem for Context Unification to the (decidable) satisfiability problem of Word Unification with regular constraints.

Ver Índice Ver Índice (0.14 Mb)

Vista previa Vista previa (0.29 Mb)

Información bibliográfica

Descripción física del libro: XX, 177 p. : gráf. ; 24 cm

ISBN: 978-84-00-08319-9

Publicación: Bellaterra (España) : Consejo Superior de Investigaciones Científicas, 2005

Referencia CSIC: 11140

Otros datos: Tesis

Adquirir la edición digital en

Este eBook está disponible en descarga gratuita

Descargas gratuitas

Descargar eBook Descargar eBook (4.6 Mb)

Este título está en nuestro catálogo electrónico desde el lunes 28 septiembre, 2015.