Aspects of Coherence in Dependence Logic
This work clarifies the theoretical properties and computational limits of a key tractability condition (k-coherence) for researchers working on dependence logic, a non-classical logic used in areas like database theory and game theory. It is an incremental theoretical contribution.
This paper investigates the concept of k-coherence in dependence logic, a property that allows complex second-order semantics to be rewritten into tractable first-order logic. The authors demonstrate that for quantifier-free dependence logic (DQF) formulas, k-coherence is equivalent to first-order rewritability. They also establish the computational complexity of deciding k-coherence, showing it is highly undecidable for general dependence logic, co-recursively enumerable for DQF formulas, and complete for the second level of the exponential hierarchy for propositional dependence logic.
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.