Labelled tableaux have been a traditional approach to define satisfiability checking procedures for Modal Logics. In many cases, they can also be used to obtain tight complexity bounds and lead to efficient implementations of reasoning tools. More recently, it has been shown that the expressive power provided by the operators characterizing Hybrid Logics (nominals and satisfiability modalities) can be used to \emph{internalize} labels, leading to well-behaved inference procedures for fairly expressive logics. The resulting procedures are attractive because they do not use external mechanisms outside the language of the logic at hand, and have good logical and computational properties. Many tableau systems based on Hybrid Logic have been investigated, with more recent efforts concentrating on Modal Logics that support data comparison operators. Here, we introduce an internalized tableau calculus for XPath, arguably one of the most prominent approaches for querying semistructured data. More precisely, we define data-aware tableaux for XPath featuring data comparison operators and enriched with nominals and the satisfiability modalities from Hybrid Logic. We prove that the calculus is sound, complete and terminating. Moreover, we show that tableaux can be explored in polynomial space, therefore establishing that the satisfiability problem for the logic is PSPACE-complete. Finally, we explore different extensions of the calculus, in particular how to handle data trees and other frame classes.

翻译：标记表一直是定义模态逻辑可满足性检验过程的传统方法。在许多情况下，它们也可用于获得紧致的复杂性界限，并实现高效推理工具的实现。最近研究表明，混合逻辑特征算子（专名和可满足性模态）所提供的表达能力可用于将标签内部化，从而为表达能力较强的逻辑构建行为良好的推理过程。这类方法具有吸引力，因为它们不使用当前逻辑语言之外的外部机制，并具有良好的逻辑与计算性质。基于混合逻辑的多种表系统已被研究，近期工作主要集中在支持数据比较算子的模态逻辑上。本文为XPath引入了一种内部化表演算——XPath无疑是查询半结构化数据最主流的方法之一。具体而言，我们为XPath定义了支持数据比较算子、并融合混合逻辑中专名与可满足性模态的数据感知表。我们证明了该演算的可靠性、完备性与终止性。此外，我们表明表可在多项式空间内展开，从而确定该逻辑的可满足性问题属于PSPACE完全问题。最后，我们探讨了该演算的多种扩展方案，特别是如何处理数据树及其他框架类。