UMA 2022
XPath (XML Path Language) es uno de los lenguajes más conocidos para realizar consultas sobre documentos XML. El lenguaje provee mecanismos para navegar la estructura de dichos documentos, y también funcionalidades para realizar consultas y operaciones sobre los mismos. El fragmento navegacional de XPath se conoce como Core-XPath. Este fragmento permite expresar propiedades estructurales de un documento XML tales como: el nombre de un atributo de un nodo, cuales son sus ancestros, descendientes, etc., pero no puede expresar condiciones referidas al contenido de un documento XML. Esta limitación de Core-XPath deja de lado, por ejemplo, la posibilidad de realizar operaciones de join de documentos XML. La extensión de Core-XPath con tests de igualdad o desigualdad permite salvar esta limitación. Esta extensión se la conoce con el nombre de Core-Data-XPath.
Core-XPath ha sido ampliamente estudiado desde una perspectiva de lógica modal; y este enfoque se ha extendido, más recientemente, a Core-Data-XPath. De particular importancia en nuestro caso es el trabajo reportado en [1]. Allí se propone una lógica llamada HXPath$_{=}$. Una de las características principales de HXPath$_{=}$ es la incorporación de expresiones de la forma $\langle \alpha = \beta \rangle$ (como así también $\langle \alpha \neq \beta \rangle$) donde $\alpha$ y $\beta$ son intuitivamente entendidas como expresiones navegacionales o de camino, mientras que $=$ (y $\neq$) son intuitivamente entendidos como operaciones de comparación entre los datos existentes al final de los caminos denotados por $\alpha$ y $\beta$. Como característica distintiva, HXPath$_{=}$ incorpora nominales y el operador de satisfacibilidad $@$ provenientes del mundo de la Lógica Híbrida [2] en su lenguaje lógico. Esto último facilita su axiomatización y permite la obtención de un resultado de completitud al estilo de Henkin.
La lógica HXPath$_{=}$ se encuentra definida sobre una base modal clásica. Nuestro trabajo propone una visión alternativa de HXPath$_{=}$ construida sobre una base modal intuicionista. Esta propuesta gana en interés ya que dota de una lectura intuicionista a Core-Data-XPath permitiéndonos distinguir entre la forma de razonar y el objeto sobre el cual razonamos.
En concreto, nuestro trabajo propone reemplazar la base modal híbrida clásica de HXPath$_{=}$ por la base modal híbrida intuicionista presentada en [3]. Tal reemplazo resulta en una nueva lógica para Core-Data-XPath la cual llamaremos IHXPathC.
Desde el punto de vista semántico, nuestra propuesta toma los modelos modales híbridos intuicionistas propuestos en [3] y los extiende con: (i) múltiples modalidades las cuales nos permiten modelar expresiones de caminos; (ii) múltiples modalidades de comparación por igualdad/desigualdad las cuales nos permiten modelar comparaciones de datos por distintos atributos. Crucialmente, las relaciones de igualdad y desigualdad sobre esta base intuicionista no son complementarias. En un contexto clásico, la igualdad puede entenderse como el complemento de la desigualdad, y vice-versa. En un contexto intuicionista, la falla de comparación por igualdad entre dos datos, no puede ser usada como prueba de que los datos son distintos.
En línea con el enfoque intuicionista propuesto en [3], en IHXPathC cada estado de conocimiento puede entenderse como un modelo de HXPath$_{=}$. Sobre esos estados de conocimiento definimos una relación de orden parcial epistémico la cual puede demostrarse preserva conocimiento. Más precisamente, al avanzar a un estado de conocimiento mayor los modelos de HXPath$_{=}$ son modificados monótonamente.
El trabajo en progreso actual busca axiomatizar la clase de modelos definida para IHXPathC usando como punto de partida el sistema axiomático para la lógica híbrida intuicionista presentado en [3], junto con el sistema axiomático para HXPath$_{=}$ presentado en [1].
El objetivo final es el de obtener una axiomatización correcta y completa para IHXPathC.
Trabajo en conjunto con: Carlos Areces (Universidad Nacional de Córdoba, Argentina), Valentin Cassano (Universidad Nacional de Córdoba, Argentina) y Raul Fervari (Universidad Nacional de Córdoba, Argentina).
Referencias
[1] Carlos Areces and Raul Fervari. Axiomatizing hybrid xpath with data. Logical Methods in Computer science, 17(3), 2021.
[2] Carlos Areces and Balder ten Cate.Hybrid Logics, pages 821–868. Elsevier, 2007.
[3] Torben Braüner. Hybrid Logic and its Proof-Theory. Springer, 2011.