paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Axiomatizing Hybrid XPath with Data

带数据的混合 XPath 的公理化
LMCS vol.Volume 17, Issue 32021匹配度 2/10 · 论文研究带数据约束的混合 XPath 的公理化、完全性与可判定性,属于逻辑与自动机、形式语义领域,与用户关注的静态分析(尤其是 ML/Agentic 程序)、LLM 与程序分析交叉、浮点或贝叶斯程序分析等核心方向无直接关联;且纯理论、无工程落地或工业案例,也未涉及 LLM/Agent。引用 4 inbox
Carlos Areces, Raul Fervari
crossref: 2026-09-10

AI 速览

一句话:为带数据约束的混合 XPath 建立可靠且强完全的公理化系统,并研究树模型公理化与可判定性。

论文研究带数据约束并扩展混合算子的 XPath 逻辑。作者首先定义 HXPath=:一种带数据的多模态 XPath 版本,加入 nominal 与混合算子 @。随后给出公理系统,并证明其相对于抽象数据模型(数据值被抽象为等价关系)是可靠且强完全的。作者还证明一个一般完全性结果,说明该系统的若干扩展在广泛帧类上仍保持完全,并给出具体实例。针对实践中常用的树模型,论文证明不存在强完全、有穷的一阶混合 XPath 公理化,并提出两种替代方案。最后引入过滤法来考察这些语言可满足性问题的可判定性。

问题
带数据约束的 XPath 在扩展混合算子后缺乏公理化与完全性结果,树模型上是否存在强完全的有穷一阶公理化以及可满足性是否可判定也不清楚。
方法
定义 HXPath= 多模态逻辑,构造公理系统,并利用一般完全性结果与过滤法分析不同帧类、树模型及可满足性。
评估
通过数学证明建立抽象数据模型上的强完全性,并证明树模型上不存在有穷一阶强完全公理化,进而提出替代方案并考察可判定性。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot1301,
  title = {Axiomatizing Hybrid XPath with Data},
  author = {Carlos Areces and Raul Fervari},
  journal = {Logical Methods in Computer Science},
  volume = {Volume 17, Issue 3},
  year = {2021},
  doi = {10.46298/lmcs-17(3:5)2021}
}