Sequent Calculi for Data-Aware Modal Logics

C. Areces, V. Cassano, D. Dutto, and R. Fervari. Sequent Calculi for Data-Aware Modal Logics. In 20th International Symposium on Logical and Semantic Frameworks, with Applications (LSFA 2025), 2025.

Download

[pdf] 

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.

BibTeX

@inProceedings{lsfa2025,
  author       = {C. Areces and
                  V. Cassano and
                  D. Dutto and
                  R. Fervari},
  title        = {Sequent Calculi for Data-Aware Modal Logics},
  booktitle = {20th International Symposium on Logical and Semantic
                  Frameworks, with Applications (LSFA 2025)},
  year         = {2025},
  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.",
}