Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos

Abriola, Sergio Alejandro

Registro:

Documento:	Tesis Doctoral
Disciplina:	matematica
Título:	Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
Título alternativo:	Model theory, proof theory, and computational aspects of logics for reasoning on data trees
Autor:	Abriola, Sergio Alejandro
Editor:	Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Filiación:	Instituto de Investigación en Ciencias de la Computación (ICC)
Publicación en la Web:	2019-11-30
Fecha de defensa:	2017-03-31
Fecha en portada:	2017
Grado Obtenido:	Doctorado
Título Obtenido:	Doctor de la Universidad de Buenos Aires en el área de Ciencias Matemáticas
Director:	Figueira, Santiago
Consejero:	Sasyk, Román
Jurado:	Caicedo, Xavier; Arenas, Marcelo; Celani, Sergio A.
Idioma:	Inglés
Formato:	PDF
Handle:	http://hdl.handle.net/20.500.12110/tesis_n6267_Abriola
PDF:	https://bibliotecadigital.exactas.uba.ar/download/tesis/tesis_n6267_Abriola.pdf
Registro:	https://bibliotecadigital.exactas.uba.ar/collection/tesis/document/tesis_n6267_Abriola
Ubicación:	Dep.MAT 006267
Derechos de Acceso:	Esta obra puede ser leída, grabada y utilizada con fines de estudio, investigación y docencia. Es necesario el reconocimiento de autoría mediante la cita correspondiente. Abriola, Sergio Alejandro. (2017). Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de http://hdl.handle.net/20.500.12110/tesis_n6267_Abriola

Resumen:

XPath es el lenguaje de consultas más ampliamente utilizado para documentos XML; es un estándar abierto y constituye una World Wide Web Consortium (W3C) Recommendation. Trabajamos con un fragmento de este lenguaje, apropiadamente reinterpretado como una lógica: XPath=, una lógica que puede ser vista como una extensión de la lógica modal básica, pero en el contexto de árboles con datos y, fundamentalmente, con la capacidad de realizar comparación de datos entre nodos. Desarrollamos la teoría de modelos de XPath=(↓), que solo puede navegar el árbol descendiendo, y XPath=(↑↓), que también puede navegar hacia arriba. Obtenemos resultados de definibilidad y separación para los dos tipos de fórmulas en XPath=: expresiones de nodo y expresiones de camino. También desarrollamos la noción de bisimulación binaria para ambos fragmentos, y demostramos un teorema de caracterización al estilo van Benthem para expresiones de camino de XPath=(↓). Encontramos axiomatizaciones ecuacionales correctas y completas para XPath=(↓) y para su fragmento libre de desigualdades de datos XPath=(↓)^-. Para demostrar completitud construimos, para cada expresión de nodo consistente, un árbol finito con datos en cuya raíz se satisface la formula. Extendemos XPath= al universo de grafos con datos, y analizamos la complejidad computacional de decidir si dos nodos en dos grafos con datos son bisimilares. Calculamos cotas ajustadas de complejidad para varios problemas de bisimilaridad y para diferentes universos de modelos. Introducimos LRV, una lógica para navegar sobre árboles con datos múltiples, y obtenemos procedimientos de decisión para el problema de satisfabilidad de LRV y algunos fragmentos al reducirlo al problema de control-state-reachability de diferentes sistemas con contadores.

Abstract:

XPath is the most widely used query language for XML documents; it is an open standard and constitutes a World Wide Web Consortium (W3C) Recommendation. We work with a fragment of this language, suitably reinterpreted as a logic: XPath=, which can be seen as an extension of basic modal logic, but in the context of data trees and, fundamentally, with the capacity to deal with data comparisons between nodes. We develop the model theory of both XPath=(↓), which can only navigate the tree downwards, and XPath=(↑↓), which can also navigate upwards. We obtain definability and separation results for the two types of formulas in XPath=: node expressions and path expressions. We also develop the notion of binary bisimulation for both fragments, and prove a van Benthem-style characterization theorem for paths expressions of XPath=(↓). Sound and complete equational axiomatizations are found for XPath=(↓) and for its data-inequality-free fragment XPath=(↓)^-. To prove completeness we construct, for every consistent node expression, a finite data tree where it is satisfied at the root. XPath= is extended to the universe of data graphs, and we analyze the computational complexity of deciding if two pointed data graphs are bisimilar. We calculate tight complexity bounds for various bisimilarity problems and different universes of models We introduce LRV, a logic to navigate over multidata trees, and obtain decision procedures for the satisfiability problem of LRV and some fragments by reducing it to the control-state reachability problem of different counter systems.

Citación:

---------- APA ----------

Abriola, Sergio Alejandro. (2017). Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos. (Tesis Doctoral. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales.). Recuperado de https://hdl.handle.net/20.500.12110/tesis_n6267_Abriola

---------- CHICAGO ----------

Abriola, Sergio Alejandro. "Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos". Tesis Doctoral, Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales, 2017.https://hdl.handle.net/20.500.12110/tesis_n6267_Abriola

Estadísticas:

Descargas totales desde :

Navegar

Colección

Tesis Doctoral