带数据的混合XPath的公理化
Axiomatizing Hybrid XPath with Data
AI总结：
本文为带数据约束的混合XPath提出可靠且强完全的公理化系统，证明其在抽象数据模型上的完全性，并探讨树模型上公理化的局限性及可判定性。
摘要：
本文介绍了带数据约束并扩展了混合算子的XPath的可靠且强完全的公理化系统。首先，我们提出HXPath=，它是带数据的XPath的多模态版本，扩展了名义词和混合算子@。然后，我们为HXPath=引入一个公理系统，并证明它相对于抽象数据模型类（即数据值被抽象为等价关系的数据模型）是强完全的。我们证明了一个类似于[BtC06]中提出的通用完全性结果，该结果确保我们所引入的公理系统的某些扩展也是完全的。通过这种方式获得的公理系统覆盖了不同框架类上的大量混合XPath语言家族，我们为此提供了具体示例。此外，我们研究了树模型（实践中广泛使用的结构）类上的公理化。我们证明，在树上不存在混合XPath的强完全、有限、一阶公理化，并提出了两种替代方案来处理这个问题。最后，我们引入过滤（filtration）方法来研究这些语言的可满足性问题的可判定性状态。
英文摘要：
In this paper we introduce sound and strongly complete axiomatizations for XPath with data constraints extended with hybrid operators. First, we present HXPath=, a multi-modal version of XPath with data, extended with nominals and the hybrid operator @. Then, we introduce an axiomatic system for HXPath=, and we prove it is strongly complete with respect to the class of abstract data models, i.e., data models in which data values are abstracted as equivalence relations. We prove a general completeness result similar to the one presented in, e.g., [BtC06], that ensures that certain extensions of the axiomatic system we introduce are also complete. The axiomatic systems that can be obtained in this way cover a large family of hybrid XPath languages over different classes of frames, for which we present concrete examples. In addition, we investigate axiomatizations over the class of tree models, structures widely used in practice. We show that a strongly complete, finitary, first-order axiomatization of hybrid XPath over trees does not exist, and we propose two alternatives to deal with this issue. We finally introduce filtrations to investigate the status of decidability of the satisfiability problem for these languages.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
