arXiv 1503.011442015-03cs.LO

团队语义中数据复杂性的可追溯边界

Tractability Frontier of Data Complexity in Team Semantics

Arnaud Durand, Juha Kontinen, Nicolas de Rugy-Altherre, Jouko Väänänen

摘要：

研究了具有团队语义的逻辑模型检测的数据复杂性。我们专注于严格和宽松的团队语义下的依赖，包含和独立逻辑公式。我们的研究结果描绘了一个清晰的易处理性/难处理性边界的数据复杂性的量化器的自由和量化的公式为每个逻辑。对于松散语义下的包含逻辑，我们将模型检测问题归结为所谓的双Horn布尔公式的可满足性问题。通过这种约简，我们给出了包含逻辑的数据复杂性在PTIME内的已知结果的另一种证明。

英文摘要：

We study the data complexity of model-checking for logics with team semantics. We focus on dependence, inclusion, and independence logic formulas under both strict and lax team semantics. Our results delineate a clear tractability/intractability frontiers in data complexity of both quantifier-free and quantified formulas for each of the logics. For inclusion logic under the lax semantics, we reduce the model-checking problem to the satisfiability problem of so-called dual-Horn Boolean formulas. Via this reduction, we give an alternative proof for the known result that the data complexity of inclusion logic is in PTIME.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

双闭时间量化约束满足问题的可处理性前沿

Tractability Frontier for Dually-Closed Temporal Quantified Constraint Satisfaction Problems

时态（约束）语言是一种关系结构，其一阶定义为有理数，其阶数为。我们在这里研究的时间约束语言的量化约束满足问题（QCSP）的复杂性。我们的主要贡献是一个二分法的限制类双封闭的时间语言。我们证明了这样一种语言的QCSP要么在多项式时间内是可解的，要么对于NP或coNP是困难的。我们的结果推广了类似的二分法QCSP的平等语言，这是关系结构定义的布尔组合的等式。

2021-09-06cs.LO

概率团队语义学和实数上存在二阶逻辑的可追溯性前沿

Tractability frontiers in probabilistic team semantics and existential second-order logic over the reals

概率团队语义是概率依赖的逻辑分析框架。我们的重点是概率包含逻辑及其扩展的公理化，复杂性和表达性。我们确定了一个自然片段的存在性二阶逻辑与添加剂真正的算术，准确地捕捉概率包含逻辑的表达能力。此外，我们将这些形式主义的线性规划，这样做得到PTIME数据复杂度的逻辑。此外，在有限结构上，我们证明了具有加性实算术的完全存在二阶逻辑只能表示NP性质。最后，我们在原子层次上给出了概率包含逻辑的一个合理而完整的公理化。

2021-12-21cs.LO

精心设计的SPARQL查询的易处理边界

The tractability frontier of well-designed SPARQL queries

我们研究了SPARQL查询的查询评估的复杂性。我们专注于设计良好的SPARQL的基本片段，仅限于AND，OPTIONAL和UNION运算符。我们的主要结果是一个结构特征的类设计良好的查询，可以在多项式时间进行评估。特别是，我们引入了一个新的宽度概念，称为支配宽度，它依赖于著名的树宽概念。我们表明，在一些复杂性理论的假设下，设计良好的查询，可以在多项式时间进行评估的类正是那些有界的统治宽度。

2018-03-27cs.DBcs.DScs.LO

类图一阶查询集的可处理性边界

The Tractability Frontier of Graph-Like First-Order Query Sets

本文研究一阶模型检验，即判定一个给定的一阶句子是否满足一个给定的有限结构。特别是，我们的目标是了解哪些句子集这个问题是易于处理的，在这个意义上的参数化复杂性理论。为此，我们定义了一个图形样的句子集的概念，该定义的灵感来自以前的工作，一阶模型检验，其中允许的连接词和量词的限制。我们的主要定理是这样的图状句子集的完全易处理性分类，这是（据我们所知）的第一个复杂性分类定理的一类句子，没有限制的连接词和量词。为了展示和证明我们的分类，我们引入并开发了一个新的复杂性理论框架，该框架建立在参数化复杂性的基础上，并包含了新的简化概念。

2014-07-13cs.CCcs.LO

基于模块化SAT的团队语义推理技术

Modular SAT-based techniques for reasoning tasks in team semantics

我们研究了团队语义中逻辑推理任务的复杂性。我们的主要重点是数据的复杂性模型检验，但我们也得到了新的结果，逻辑定义的计数和枚举问题。我们的方法是基于这些问题的模块化减少到相应的问题的各类布尔公式。我们说明了我们的方法，通过几个新的易处理性/难处理性的结果。

2022-04-01cs.LO

缺省逻辑中的异常值检测：易处理性/难处理性边界

Outlier detection in default logics: the tractability/intractability frontier

University of Calabria（卡拉布里亚大学）；Jerusalem College of Engineering（耶路撒冷工程学院）

在默认理论中，离群值表示具有意外属性的文字集。在以前的论文中，我们定义了缺省逻辑中的离群点，并研究了它们的形式性质。具体来说，我们已经研究了异常值检测问题的计算复杂性，并证明，虽然它们通常是棘手的，有趣的易处理的情况下，可以挑选出来。根据这些结果，我们在这里研究离群点检测问题的易处理性边界，通过分析它（i）考虑离群点检测问题，（ii）参考默认逻辑片段，（iii）采用离群点的概念。对于第（i）点，我们将考虑三个日益复杂的问题，分别称为离群点-证人识别，离群点识别和离群点存在。至于第（ii）点，当我们寻找可以有效地进行离群点检测的条件时，注意力将限于无析取命题缺省理论的子集。至于第（iii）点，我们将参考[ABP 08]的离群值概念和一个新的更具限制性的概念，称为强离群值。在复杂性结果的基础上，我们提出了一个多项式时间算法来计算拟无循环正态一元缺省理论中所有有界强离群点。我们的一些易处理性的结果依赖于增量引理，提供了条件的一个contrult逻辑片段具有单调的行为。最后，为了表明我们处理的DL的简单片段仍然足够丰富，以解决有趣的问题，因此，我们证明的易处理性结果不仅在理论方面是有趣的，这些片段的表达能力的见解，通过显示正常的一元理论表达所有NL查询，从而间接回答了考茨和塞尔曼提出的问题。

2013-10-30cs.AIcs.CCcs.LO

更多相关论文收起更多论文

绘制某些合取查询查询的可处理性边界

Charting the Tractability Frontier of Certain Conjunctive Query Answering

不确定数据库定义为不需要满足主键的关系数据库。这样的数据库的修复（或可能世界）通过选择最大数量的元组而不选择具有相同主键码值的两个不同元组来获得。对于布尔查询q，决策问题CERTAINTY（q）将不确定数据库db作为输入，并询问db的每次修复是否满足q。我们的主要重点是非循环布尔合取查询没有自我加入。以前的工作已经引入了这种查询的（有向）攻击图的概念，并证明了CERTAINTY（q）是一阶可表达的当且仅当q的攻击图是非循环的。本文研究了确定性（q）的易处理性和难处理性之间的界限。我们首先将攻击图中的循环分类为弱或强，然后证明以下内容。如果一个查询q的攻击图包含一个强循环，则CERTAINTY（q）是coNP完全的。如果q的攻击图不包含强圈且其每个弱圈都是终端的（即，没有边从圈中的顶点通向圈外的顶点），则CERTAINTY（q）在P中。然后我们部分地解决唯一剩余的开放情况，即，当攻击图中存在非终结环且不存在强环时，最后，我们在概率数据库上建立了CERTAINTY（q）的复杂性和评估q之间的关系。

2013-01-06cs.DBcs.LO

具有团队语义的线性时间时态逻辑：表达性和复杂性

Linear-time Temporal Logic with Team Semantics: Expressivity and Complexity

研究了具有团队语义的模型检验线性时态逻辑（TeamLTL）的表达性和复杂性。TeamLTL，尽管是一个纯粹的模态逻辑，但能够定义超属性，即，与多个执行跟踪相关的属性。TeamLTL最近才被引入，关于它的表达能力和模型检验问题，只有很少的结果是已知的。我们将TeamLTL的表达性与通过用迹和命题量词（HyperLTL和HyperQPTL）扩展LTL获得的超性质的逻辑联系起来。通过这样做，我们得到了一些模型检验的TeamLTL结果，并确定其不可判定性边界。特别是，我们证明了任何向下封闭的TeamLTL扩展的所谓的左平坦片段的模型检验的可判定性。此外，我们建立了具有布尔析取和包含原子的TeamLTL的模型检验问题是不可判定的。

2021-11-23cs.CCcs.LO

包含逻辑中的复杂性假设

Complexity Thresholds in Inclusion Logic

具有团队语义的逻辑为复杂性类的逻辑表征提供了替代手段。依赖和独立逻辑都被认为可以捕获非确定性的多项式时间，并且这些逻辑中的易处理性的边界被相对较好地理解。包含逻辑类似于这些基于团队的逻辑形式主义，除了它对应于有序模型中的确定性多项式时间。在这篇文章中，我们研究包含逻辑的语法片段和不同的复杂性类之间的连接，在两个计算问题：最大的子组成员和模型检验问题的一个固定的包含逻辑公式。我们发现，非常简单的量词免费公式与一个或两个包含原子产生的这些问题是完整的（非确定性）对数空间和多项式时间的实例。此外，我们提出了一个片段的包含逻辑，捕捉非确定性的对数空间有序模型。

2019-03-26cs.CCcs.DBcs.LO