Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Sequent Calculi for Data-Aware Modal Logics

Carlos Areces, Valentin Cassano, Danae Dutto, Raul Fervari

TL;DR

This paper develops a Gentzen-style sequent calculus for the data-aware modal logic \text{HXPath}_{\rm D}, unifying XPath-like navigation with data-value comparisons in hybrid data models. It proves soundness, rule invertibility, and completeness (via a translation from a Hilbert system), and establishes cut elimination for the calculus, providing a solid proof-theoretic foundation. The work further relates the calculus to a hybrid-logic fragment, shows a corresponding subsystems' correspondence with existing sequent systems, and outlines directions for termination, proof-search optimization, and extensions to richer navigational features. Overall, the results offer a rigorous proof-theoretic framework for analyzing data-rich graph query languages and set the stage for extending these techniques to broader modal systems.

Abstract

Data-aware modal logics offer a powerful formalism for reasoning about semi-structured queries in languages such as DataGL, XPath, and GQL. In brief, these logics can be viewed as modal systems capable of expressing both reachability statements and data-aware properties, such as value comparisons. One particularly expressive logic in this landscape is HXpathD, a hybrid modal logic that captures not only the navigational core of XPath but also data comparisons, node labels (keys), and key-based navigation operators. While previous work on HXpathD has primarily focused on its model-theoretic properties, in this paper we approach HXpathD from a proof-theoretic perspective. Concretely, we present a sound and complete Gentzen-style sequent calculus for HXpathD. Moreover, we show all rules in this calculus are invertible, and that it enjoys cut elimination. Our work contributes to the proof-theoretic foundations of data-aware modal logics, and enables a deeper logical analysis of query languages over graph-structured data. Moreover, our results lay the groundwork for extending proof-theoretic techniques to a broader class of modal systems.

Sequent Calculi for Data-Aware Modal Logics

TL;DR

This paper develops a Gentzen-style sequent calculus for the data-aware modal logic \text{HXPath}_{\rm D}, unifying XPath-like navigation with data-value comparisons in hybrid data models. It proves soundness, rule invertibility, and completeness (via a translation from a Hilbert system), and establishes cut elimination for the calculus, providing a solid proof-theoretic foundation. The work further relates the calculus to a hybrid-logic fragment, shows a corresponding subsystems' correspondence with existing sequent systems, and outlines directions for termination, proof-search optimization, and extensions to richer navigational features. Overall, the results offer a rigorous proof-theoretic framework for analyzing data-rich graph query languages and set the stage for extending these techniques to broader modal systems.

Abstract

Data-aware modal logics offer a powerful formalism for reasoning about semi-structured queries in languages such as DataGL, XPath, and GQL. In brief, these logics can be viewed as modal systems capable of expressing both reachability statements and data-aware properties, such as value comparisons. One particularly expressive logic in this landscape is HXpathD, a hybrid modal logic that captures not only the navigational core of XPath but also data comparisons, node labels (keys), and key-based navigation operators. While previous work on HXpathD has primarily focused on its model-theoretic properties, in this paper we approach HXpathD from a proof-theoretic perspective. Concretely, we present a sound and complete Gentzen-style sequent calculus for HXpathD. Moreover, we show all rules in this calculus are invertible, and that it enjoys cut elimination. Our work contributes to the proof-theoretic foundations of data-aware modal logics, and enables a deeper logical analysis of query languages over graph-structured data. Moreover, our results lay the groundwork for extending proof-theoretic techniques to a broader class of modal systems.

Paper Structure

This paper contains 9 sections, 9 theorems, 24 equations, 2 figures, 1 table.

Table of Contents

  1. Introduction
  2. Hybrid XPath with Data
  3. A Sequent Calculus for $\text{\rm HXPath}_{\rm D}$
  4. Soundness
  5. Invertibility of Rules
  6. Completeness
  7. Cut Elimination
  8. A Sequent System for Hybrid Logic
  9. Final Comments

Key Result

Proposition 4

[proposition]prop:abbrv $\amodel,n \Vdash \langle\alpha\rangle\varphi$ iff $\hbox{exists $n' \in \mathrm{N}$ s.t.},~ \amodel,n,n' \Vdash\alpha$ and $\amodel,n' \Vdash \varphi$. Moreover, $\amodel,n \Vdash [\alpha=_{\xspace\mathsf{c}\xspace}\beta]$ iff for all $n',n"\in \mathrm{N}$, $\amodel,n,n' \Vd

Figures (2)

  • Figure 1: Example of a Data Graph
  • Figure 2: Sequent Calculus $\mathbf{G}$ for $\text{\rm HXPath}_{\rm D}$.

Theorems & Definitions (26)

  • Definition 1
  • Definition 2
  • Definition 3
  • Proposition 4
  • Example 1
  • Definition 5
  • Definition 6
  • Definition 7
  • Lemma 8: Soundness
  • proof
  • ...and 16 more