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

Mostrar todas las versiones(3)

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...

Descripción completa

Detalles Bibliográficos
Autor principal: Abriola, Sergio Alejandro
Otros Autores: Figueira, Santiago Daniel
Formato: Tesis doctoral publishedVersion
Lenguaje:Inglés
Publicado: Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2017
Materias:
XPATH=
DATA-AWARE LOGICS
BISIMULATION
MODEL THEORY
EXPRESSIVITY
PROOF THEORY
COMPUTATIONAL COMPLEXITY
AUTOMATA
SATISFIABILITY
BRANCHING COUNTER SYSTEMS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n6267_Abriola
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id tesis:tesis_n6267_Abriola
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Inglés
orig_language_str_mv eng
topic XPATH=
DATA-AWARE LOGICS
BISIMULATION
MODEL THEORY
EXPRESSIVITY
PROOF THEORY
COMPUTATIONAL COMPLEXITY
AUTOMATA
SATISFIABILITY
BRANCHING COUNTER SYSTEMS
spellingShingle XPATH=
DATA-AWARE LOGICS
BISIMULATION
MODEL THEORY
EXPRESSIVITY
PROOF THEORY
COMPUTATIONAL COMPLEXITY
AUTOMATA
SATISFIABILITY
BRANCHING COUNTER SYSTEMS
Abriola, Sergio Alejandro
Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
topic_facet XPATH=
DATA-AWARE LOGICS
BISIMULATION
MODEL THEORY
EXPRESSIVITY
PROOF THEORY
COMPUTATIONAL COMPLEXITY
AUTOMATA
SATISFIABILITY
BRANCHING COUNTER SYSTEMS
description 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.
author2 Figueira, Santiago Daniel
author_facet Figueira, Santiago Daniel
Abriola, Sergio Alejandro
format Tesis doctoral
Tesis doctoral
publishedVersion
author Abriola, Sergio Alejandro
author_sort Abriola, Sergio Alejandro
title Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
title_short Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
title_full Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
title_fullStr Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
title_full_unstemmed Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
title_sort teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos
publisher Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
publishDate 2017
url https://hdl.handle.net/20.500.12110/tesis_n6267_Abriola
work_keys_str_mv AT abriolasergioalejandro teoriademodelosteoriadepruebayaspectoscomputacionalesdelogicaspararazonarsobrearbolescondatos
AT abriolasergioalejandro modeltheoryprooftheoryandcomputationalaspectsoflogicsforreasoningondatatrees
_version_ 1831982115225337856
spelling tesis:tesis_n6267_Abriola2025-03-31T21:42:53Z Teoría de modelos, teoría de prueba, y aspectos computacionales de lógicas para razonar sobre árboles con datos Model theory, proof theory, and computational aspects of logics for reasoning on data trees Abriola, Sergio Alejandro Figueira, Santiago Daniel XPATH= DATA-AWARE LOGICS BISIMULATION MODEL THEORY EXPRESSIVITY PROOF THEORY COMPUTATIONAL COMPLEXITY AUTOMATA SATISFIABILITY BRANCHING COUNTER SYSTEMS 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. 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. Fil: Abriola, Sergio Alejandro. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales 2017-03-31 info:eu-repo/semantics/doctoralThesis info:ar-repo/semantics/tesis doctoral info:eu-repo/semantics/publishedVersion application/pdf eng info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n6267_Abriola

Ejemplares similares