Cargando Eventos
Título: Lógicas para razonar sobre grafos con datos
Director: Santiago Figueira
Director adjunto: Diego Figueira
Consejera de estudios: Teresa Krick
Jurados:
Dra. Flavia Bonomo, UBA & CONICET
Dra. Magdalena Ortiz, TUW, Austria
Dr. Domagoj Vrgoc, PUC, Chile
Resumen:
En esta tesis analizamos una serie de problemas relevantes en el área de Teoría de Bases de Datos, usando herramientas lógicas, modelo-teóricas y computacionales. Nos enfocamos particularmente en el caso donde la información se almacena en una estructura con forma de grafo etiquetado.Estudiamos la inconsistencia de una base de datos respecto a un conjunto de restricciones (ontología). Por un lado, existen varias maneras de formalizar este escenario, que depende tanto de las clases de estructuras a considerar como del lenguaje ontológico utilizado para razonar sobre tales estructuras. Por otro lado, existen muchas formas de lidiar con bases de datos inconsistentes, ya sea tratando de eliminar la inconsistencia manipulando la base de datos, o manteniendo el estado actual de la base pero identificando la información certera, es decir, los datos que prevalecerán independientemente del tipo de modificación que se haga sobre la base original.Una reparación de una base de datos inconsistente es una base de datos consistente que se obtiene a partir de la original realizando una cantidad mínima de modificaciones. Introdujimos una semántica de satisfacción global respecto a restricciones expresadas en GXPath (una lógica que permite expresar propiedades de nodos y caminos sobre la base de datos en forma de grafo), y analizamos el problema de hallar reparaciones de una base de datos con forma de grafo. Las nociones de reparación usadas se formalizaron en dos categorías: subreparaciones, que se obtienen mediante el proceso de eliminación de información; y superreparaciones, que se obtienen mediante el proceso de agregado de información. Con todo el poder expresivo de GXPath, demostramos que el problema de hallar superrepaciones es indecidible, mientras que el problema de hallar subreparaciones es NP-completo. Abordamos los mismos problemas respecto a fragmentos de GXPath, en particular GXPath-pos (expresiones positivas de GXPath) y Core-GXPath (con la estrella de Kleene restringido a átomos). Si bien los problemas de subreparaciones y superreparaciones siguen siendo NP-completos respecto a expresiones de camino, demostramos que los respectivos problemas respecto a expresiones de nodo son ambos polinomiales.
Se abordó el problema de Fininte Ontology Mediated Query Answering (FOMQA), una variante de Ontology Mediated Query Answering (OMQA) en la que se asume que el mundo representado es finito, y por lo tanto, solo se consideran modelos finitos de la ontología. Estudiamos la propiedad de controlabilidad finita, es decir, cuándo FOMQA y OMQA son equivalentes, para fragmentos de C2RPQ (Conjunctive Regular Path Queries con reverso). Para una clase de grafos S, consideramos los fragmentos C2RPQ(S) de C2RPQ como las consultas cuyo grafo subyacente pertenece a S. Clasificamos completamente los fragmentos controlables finitamente y los que no lo son, bajo: dependencias de inclusión, reglas frontier-guarded, reglas frontier-one (tanto con como sin constantes), y de manera más general bajo restricciones de lógica de primer orden con guarded-negation. Para los fragmentos controlables finitamente, mostramos una reducción al problema de satisfacibilidad para la lógica de primer orden con guarded-negation, lo que da lugar a un algoritmo en 2EXPTIME (en complejidad combinada) para el problema correspondiente de (F)OMQA.En otra línea de trabajo, propusimos un nuevo lenguaje de consulta denominado CPDL+, que extiende a la Propositional Dynamic Logic (PDL), con una nueva construcción sintáctica para “programas conjuntivos”, compatible con los demás operadores sintácticos de PDL. Mostramos que ciertas subclases naturales de CPDL+ pueden definirse en términos del tree-width de los grafos subyacentes de las fórmulas. Demostramos que la clase de fórmulas CPDL+ con tree-width 2 es equivalente a PDL con intersección de programas y que también coincide con las fórmulas de CPDL+ de tree-width 1. Sin embargo, más allá de tree-width 2, incrementar el tree-width aumenta estrictamente el poder expresivo. Caracterizamos el poder expresivo de cada clase de fórmulas con tree-width fijo mediante un juego de bisimulación con piedritas. Basándonos en esta caracterización, demostramos que CPDL+ posee una propiedad de modelo “tree-like”. Probamos que el problema de satisfacibilidad para CPDL+ es decidible en 3EXPTIME y es 2EXPTIME-completo para el fragmento de tree-width acotado. Finalmente, establecemos que el problema de model checking para fórmulas con tree-width fijo está en PTIME, a diferencia de la clase completa de CPDL+, en donde solo tenemos una cota de PTIME con acceso a un oráculo NP.