用数据公理化混合XPath
摘要：XPath数据约束扩展与混合操作符的完备公理化的声音和强大的界定。首先，我们介绍HXPath=，这是一个具有数据的多模态版本，扩展了名词和混合操作符@。然后，我们引入了HXPath=的公理系统，并证明它相对于抽象数据模型的类是强大的完整的，即数据值被抽象为等价关系的数据模型。我们证明了一个类似于[BtC06]中的通用完整性结果，保证了我们引入的公理系统的某些扩展也是完整的。通过这种方式可以获得的公理系统涵盖了不同类别的框架上的大量混合XPath语言家族，我们提供了具体的示例。另外，我们研究了在树模型类别上的公理化。我们证明强大的完备、有限、一阶的树形混合XPath公理化不存在，并提出了两种处理这个问题的替代方案。最后，我们引入过滤来研究这些语言的可满足性问题的可判定性状态。
作者：Carlos Areces, Raul Fervari
论文ID：2004.00124
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22