Sequent Calculi for Data-Aware Modal Logics

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 HXPath D , 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 HXPath D has primarily focused on its model-theoretic properties, in this paper we approach HXPath D from a proof-theoretic perspective.Concretely, we present a sound and complete Gentzen-style sequent calculus for HXPath D .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.