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.

翻译：数据感知模态逻辑为在DataGL、XPath和GQL等语言中进行半结构化查询推理提供了强大的形式化工具。简而言之，这些逻辑可视为既能表达可达性陈述，又能表达数据感知属性（如值比较）的模态系统。在此领域中，HXpathD是一种表达能力特别强的逻辑，它是一种混合模态逻辑，不仅能捕获XPath的导航核心，还能处理数据比较、节点标签（键）以及基于键的导航运算符。尽管先前关于HXpathD的研究主要集中于其模型论性质，本文则从证明论视角探讨HXpathD。具体而言，我们为HXpathD提出了一种可靠且完备的Gentzen风格相继式演算。此外，我们证明了该演算中的所有规则都是可逆的，并且它满足切割消除性质。我们的工作有助于奠定数据感知模态逻辑的证明论基础，并使得对图结构数据查询语言进行更深入的逻辑分析成为可能。此外，我们的结果为将证明论技术扩展至更广泛的模态系统类别奠定了基础。