@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.",
}