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.

翻译：暂无翻译