Dependence logic extends first-order logic with dependence atoms asserting that the value of a variable is determined by the values of certain other variables. The semantics of dependence logic has a second-order character and involves sets of assignments, called teams, instead of individual assignments as in the classical Tarski semantics. Since the model-checking problem is known to be NP-complete even for quantifier-free dependence logic (DQF) formulas, researchers have pursued conditions on formulas that make this problem tractable. In 2010, Jarmo Kontinen introduced the notion of k-coherence for dependence logic formulas, where k is a positive integer. This notion asserts that if the formula is satisfied in a structure by all k-element subteams of a given team, then the given team itself satisfies the formula. It has been proved that k-coherent DQF-formulas have a tame model-checking problem, because such formulas admit a first-order rewriting. In this paper, we investigate the structural and algorithmic aspects of coherence. We show that if a DQF-formula is first-order ewritable, then it is k-coherent for some positive integer k. Thus, for DQF-formulas, coherence is equivalent to first-order rewritability. Furthermore, we show that an analogous result holds for universally quantified dependence logic formulas under a stronger notion of coherence. After this, we focus on the complexity of deciding if a given dependence logic formula is k-coherent. We establish that this decision problem is highly undecidable for arbitrary dependence logic formulas, while for DQF-formulas this problem is co-recursively enumerable. Furthermore, we pinpoint the computational complexity of the coherence problem for propositional dependence logic formulas by showing that this problem is complete for the second level of the exponential hierarchy.

翻译：依赖逻辑通过依赖原子扩展了一阶逻辑，这些原子断言某个变量的值取决于其他某些变量的值。依赖逻辑的语义具有二阶特征，并涉及赋值集合（称为团队），而非经典塔尔斯基语义中的单个赋值。由于即使是无量词依赖逻辑（DQF）公式的模型检验问题也被认为是NP完全的，研究人员一直在寻找使该问题易于处理的公式条件。2010年，Jarmo Kontinen引入了依赖逻辑公式的k-相干性概念，其中k为正整数。该概念断言：如果公式在某个结构中被给定团队的所有k元素子团队满足，则给定团队本身满足该公式。已证明k-相干的DQF公式具有良性的模型检验问题，因为此类公式允许一阶重写。本文研究了相干性的结构和算法方面。我们证明，如果一个DQF公式是一阶可重写的，则对于某个正整数k，它是k-相干的。因此，对于DQF公式，相干性等价于一阶可重写性。此外，我们证明在更强的相干性概念下，全称量化的依赖逻辑公式也有类似结果。随后，我们聚焦于判定给定依赖逻辑公式是否为k-相干的复杂性。我们确定，对于任意依赖逻辑公式，该判定问题是高度不可判定的，而对于DQF公式，该问题是共递归可枚举的。此外，我们通过证明命题依赖逻辑公式的相干性问题对于指数层次第二级是完全的，精确刻画了其计算复杂性。