专栏首页arxiv.org翻译专栏用数据公理化混合XPath (CS.LD)
原创

用数据公理化混合XPath (CS.LD)

在本文中,我们介绍了具有混合约束扩展的数据约束的XPath健全且完全完备的公理化。首先,我们介绍HXPath =,它是XPath的多模式版本,其数据扩展了标称值和混合运算符@。然后,我们引入了一个针对HXPath =的公理系统,并且证明了它相对于抽象数据模型的类(即其中将数据值抽象为等价关系的数据模型)是非常完整的。我们证明了一个完整的完整性结果,类似于Blackburn和《十个凯特2006》中提出的那样,可以确保我们引入的公理系统的某些扩展也完整。可以通过这种方式获得的公理系统涵盖了不同类别的框架上的大量混合XPath语言家族,我们将给出具体示例。此外,我们研究了广泛用于实践中的树模型类结构的公理化。我们显示了在树上不存在完全完整的,有限的,混合XPath的一阶公理化,并且我们提出了两种替代方法来解决此问题。最后,我们引入过滤来调查这些语言的可满足性问题的可判定性状态。

原文标题:Axiomatizing Hybrid XPath with Data

原文: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., Blackburn and ten Cate 2006, 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, and 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, finite, 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.

原文作者:Carlos Areces, Raul Fervari

原文地址:https://arxiv.org/abs/2004.00124

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 通过扩展的沟MIDI数据集提高鼓转录的感知质量(CS.SD)

    分类器指标(例如准确性和F量度得分)通常充当下游任务性能的代理。对于使用预测标签作为输入的生成系统而言,只有在其与生成的输出的感知质量一致的情况下,准确性才是一...

    蔡小雪7100294
  • 用于任务感知的持续学习的条件通道门控网络(CS.CV)

    当针对一系列学习问题进行优化时,卷积神经网络会遭受灾难性的遗忘:当它们满足当前训练示例的目标时,它们在先前任务上的表现将急剧下降。在这项工作中,我们引入了一个新...

    蔡小雪7100294
  • 多语言姿态检测:加泰罗尼亚独立语料库(CS.CL)

    姿态检测旨在确定给定文本相对于特定主题或主张的态度。尽管最近几年对姿势检测进行了很好的研究,但大多数工作都集中在英语上。这主要是由于其他语言中相对缺少带注释的数...

    蔡小雪7100294
  • 线性回归与最小二乘法 | 机器学习笔记

    这篇笔记会将几本的线性回归概念和最小二乘法。 在机器学习中,一个重要而且常见的问题就是学习和预测特征变量(自变量)与响应的响应变量(应变量)之间的函数关系 ...

    用户1332428
  • [计算机视觉论文速递] 2018-04-28

    [1]《View Extrapolation of Human Body from a Single Image》

    Amusi
  • 第5篇:对ATAC-Seq/ChIP-seq的质量评估(二)——ChIPQC

    第4篇:对ATAC-Seq/ChIP-seq的质量评估(一)——phantompeakqualtools

    生信技能树
  • VsDoc for jQuery

    Microsoft 现在完全支持 jQuery 并将它集成在ASP.NET MVC 框架。jQuery-vsdoc.js文件,该文件对串连的jQuery sel...

    张善友
  • 黑珑科技blackdragon.com被京东收购

    有媒体报道,JD.com(京东)已经在2016年底至2017年初时悄悄收购了英文单词组合域名blackdragon.com。可是“京东”两字与“bl...

    躲在树上的域小名
  • SAP ABAP Netweaver和Hybris Commerce的开发license

    https://help.sap.com/viewer/109b81286c531014a6ae86cae80fc783/7.0.33/en-US/a7512c...

    Jerry Wang
  • AbstractQueuedSynchronizer 源码分析

    AQS是通过CHL队列来实现锁请求阻塞列表的。可以通过acquire(int arg)来分析,当前线程竞争锁时的流程,然后再通过release(int arg)...

    wannshan

扫码关注云+社区

领取腾讯云代金券