论文标题
与数据的Axiomat化混合XPath
Axiomatizing Hybrid XPath with Data
论文作者
论文摘要
在本文中，我们介绍了声音和强烈完整的公理，以通过与混合操作员扩展的数据约束进行XPATH。首先，我们提出HXPATH =是带有数据的XPATH的多模式版本，使用名义和混合操作员 @延伸。然后，我们引入了HXPATH =的公理系统，并且我们证明它在抽象数据模型类别（即数据值中被抽象为等效关系的数据模型）非常强。我们证明了类似于[BTC06]中提出的一般完整性结果，该结果可确保我们引入的公理系统的某些扩展也已完成。可以以这种方式获得的公理系统涵盖了不同类别的框架上的大型混合XPath语言，我们为此提供了具体的示例。此外，我们研究了树型类别的公理室，这些结构在实践中广泛使用。我们表明，不存在对树上混合XPath的强烈完整的，一阶的公理化，我们提出了两种解决此问题的替代方案。我们最终介绍过滤，以研究这些语言可满足性问题的可决定性状态。
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.
