Search

We introduce a new framework for a descriptive complexity approach to arithmetic computations. We define a hierarchy of classes based on the idea of counting assignments to free function variables in first-order formulae. We completely determine the inclusion structure and show that #P and # AC 0 appear as classes of this hierarchy. In this way, we unconditionally place # AC 0 properly in a strict hierarchy of arithmetic classes within #P. Furthermore, we show that some of our classes admit efficient approximation in the sense of FPRAS. We compare our classes with a hierarchy within #P defined in a model-theoretic way by Saluja et al. and argue that our approach is better suited to study arithmetic circuit classes such as # AC 0 which can be descriptively characterized as a class in our framework.

We prove two completeness results, one for the extension of dependence logic by a monotone generalized quantifier Q with weak interpretation, weak in the meaning that the interpretation of Q varies with the structures. The second result considers the extension of dependence logic where Q is interpreted as "there exists uncountable many." Both of the axiomatizations are shown to be sound and complete for FO(Q) consequences., 17 pages

In this paper, we introduce a logic based on team semantics, called \(\mathbf {FOT}\), whose expressive power coincides with first-order logic both on the level of sentences and (open) formulas, and we also show that a sublogic of \(\mathbf {FOT}\), called \(\mathbf {FOT}^\downarrow \), captures exactly downward closed first-order team properties. We axiomatize completely the logic \(\mathbf {FOT}\), and also extend the known partial axiomatization of dependence logic to dependence logic enriched with the logical constants in \(\mathbf {FOT}^\downarrow \).

We investigate implication problems for keys and independence atoms in relational databases. For keys and unary independence atoms we show that finite implication is not finitely axiomatizable, and establish a finite axiomatization for general implication. The same axiomatization is also sound and complete for finite and general implication of unary keys and independence atoms, which coincide. We show that the general implication of keys and unary independence atoms and of unary keys and general independence atoms is decidable in polynomial time. For these two classes we also show how to construct Armstrong relations. Finally, we establish tractable conditions that are sufficient for certain classes of keys and independence atoms not to interact. For unary independence atoms and keys, general implication is finitely axiomatizable but finite implication is not.Finite and general implication of unary keys and independence atoms coincide and enjoy a finite axiomatization.General implication of unary independence atoms and keys is decidable in polynomial time.General implication of unary keys and independence atoms is decidable in polynomial time.There are tractable conditions that are sufficient for some classes of keys and independence atoms not to interact.

We study definability of second-order generalized quantifiers. We show that the question whether a second-order generalized quantifier Q1 is definable in terms of another quantifier Q2, the base logic being monadic second-order logic, reduces to the question if a quantifier Q1⋆ is definable in FO(Q2⋆

Dependence logic, introduced in Väänänen (2007) [11], cannot be axiomatized. However, first-order consequences of dependence logic sentences can be axiomatized, and this is what we shall do in this paper. We give an explicit axiomatization and prove the respective Completeness Theorem.

We study fragments of dependence logic defined either by restricting the number k of universal quantifiers or the width of dependence atoms in formulas. We find the sublogics of existential second-order logic corresponding to these fragments of dependence logic. We also show that these both ways of defining fragments of dependence logic give rise to a hierarchy in expressive power with respect to k., Comment: 21 pages

We show that for any pair $\phi$ and $\psi$ of contradictory formulas of dependence logic there is a formula $\theta$ of the same logic such that $\phi\equiv\theta$ and $\psi\equiv\neg\theta$. This generalizes a result of Burgess.

In this paper, we study the expressive power of the extension of first-order logic by the unary second-order majority quantifier Most1. In 1 it was shown that the extension of FO by second-order majority quantifiers of all arities describes exactly the problems in the counting hierarchy. We consider first certain sublogics of FO(Most1) over unary vocabularies. We show that over unary vocabularies the logic MSO(R), where MSO is monadic second-order logic and R is the first-order Rescher quantifier, can be characterized by Presburger arithmetic, whereas the logic MSO(Rn)n∈Z+, where Rn is the nth vectorization of R, corresponds to the Δ0-fragment of arithmetic. Then we show that FO(Most1)⩾MSO(Rn)n∈Z+ and that, on unary vocabularies, FO(Most1) collapses to uniform-TC0. Using this collapse, we show that first-order logic with the binary second-order majority quantifier is strictly more expressive than FO(Most1) over the empty vocabulary. On the other hand, over strings, FO(Most1) is shown to capture the linear fragment of the counting hierarchy. Finally we show that, over non-unary vocabularies, FO(Most1) can express problems complete via first-order reductions for each level of the counting hierarchy.

We study second order generalized quantifiers on finite structures. One starting point of this research has been the notion of definability of Lindstrom quantifiers. We formulate an analogous notion for second order generalized quantifiers and study definability of second order generalized quantifiers in terms of Lindstrom quantifiers.

We study the expressive power of open formulas of dependence logic introduced in Väänänen [Dependence logic (Vol. 70 of London Mathematical Society Student Texts), 2007]. In particular, we answer a question raised by Wilfrid Hodges: how to characterize the sets of teams definable by means of identity only in dependence logic, or equivalently in independence friendly logic.

In this article we give a logical characterization of the counting hierarchy. The counting hierarchy is the analogue of the polynomial hierarchy, the building block being Probabilistic polynomial time PP instead of NP. We show that the extension of first-order logic by second-order majority quantifiers of all arities describes exactly the problems in the counting hierarchy. We also consider extending the characterization to general proportional quantifiers Q k r interpreted as “more than an r -fraction of k -ary relations”. We show that the result holds for rational numbers of the form s /2 m but for any other 0 < r < 1 the corresponding logic satisfies the 0-1 law.

We consider collective quantification in natural language. For many years the common strategy in formalizing collective quantification has been to define the meanings of collective determiners, quantifying over collections, using certain type-shifting operations. These type-shifting operations, i.e., lifts, define the collective interpretations of determiners systematically from the standard meanings of quantifiers. All the lifts considered in the literature turn out to be definable in second-order logic. We argue that second-order definable quantifiers are probably not expressive enough to formalize all collective quantification in natural language.

Directed acyclic graphs (DAGs) constitute a qualitative representation for conditional independence (CI) properties of a probability distribution. It is known that every CI statement implied by the topology of a DAG is witnessed over it under a graph-theoretic criterion of d-separation. Alternatively, all such implied CI statements are derivable from the local independencies encoded by a DAG using the so-called semi-graphoid axioms. We consider Labeled Directed Acyclic Graphs (LDAGs) modeling graphically scenarios exhibiting context-specific independence (CSI). Such CSI statements are modeled by labeled edges, where labels encode contexts in which the edge vanishes. We study the problem of identifying all independence statements implied by the structure and the labels of an LDAG. We show that this problem is coNP-hard for LDAGs and formulate a sound extension of the semi-graphoid axioms for the derivation of such implied independencies. Finally we connect our study to certain qualitative versions of independence ubiquitous in database theory and teams semantics.

We classify the computational complexity of the satisfiability, validity and model-checking problems for propositional independence and inclusion logic and their extensions by the classical negation.

We study the expressive power of fragments of inclusion and independence logic defined by restricting the number k of universal quantifiers in formulas. Assuming the so-called strict semantics for these logics, we relate these fragments of inclusion and independence logic to sublogics ESO_f(k\forall) of existential second-order logic, which in turn are known to capture the complexity classes NTIME_{RAM}(n^k).

In this paper we study the expressive power of Horn-formulae in dependence logic and show that they can express NP-complete problems. Therefore we define an even smaller fragment D-Horn* and show that over finite successor structures it captures the complexity class P of all sets decidable in polynomial time. Furthermore we study the question which of our results can ge generalized to the case of open formulae of D-Horn* and so-called downwards monotone polynomial time properties of teams.

We present a complete finite axiomatization of the unrestricted implication problem for inclusion and conditional independence atoms in the context of dependence logic. For databases, this result implies a finite axiomatization of the unrestricted implication problem for inclusion, functional, and embedded multivalued dependencies in the unirelational case. We also indicate the generality of our approach by showing the analogous result for inclusion and embedded join dependencies.

We characterize the expressive power of extensions of Dependence Logic and Independence Logic by monotone generalized quantifiers in terms of quantifier extensions of existential second-order logic., 9 pages

We study the extension of dependence logic $$\mathcal {D}$$D by a majority quantifier $$\mathsf{M}$$M over finite structures. We show that the resulting logic is equi-expressive with the extension of second-order logic by second-order majority quantifiers of all arities. Our results imply that, from the point of view of descriptive complexity theory, $$\mathcal {D}(\mathsf{M})$$D(M) captures the complexity class counting hierarchy. We also obtain characterizations of the individual levels of the counting hierarchy by fragments of $$\mathcal {D}(\mathsf{M})$$D(M).

We study logics defined in terms of second-order monadic monoidal and groupoidal quantifiers. These are generalized quantifiers defined by monoid and groupoid word-problems, equivalently, by regular and context-free languages. We give a computational classification of the expressive power of these logics over strings with varying built-in predicates. In particular, we show that ATIME(n) can be logically characterized in terms of second-order monadic monoidal quantifiers.

We study logics defined in terms of so-called second-order monadic groupoidal quantifiers. These are generalized quantifiers defined by groupoid word-problems or equivalently by context-free languages. We show that, over strings with built-in arithmetic, the extension of monadic second-order logic by all second-order monadic groupoidal quantifiers collapses to its fragment ${{\rm mon-}Q^1_{{\rm Grp}}}{\text{\rm FO}}$. We also show a variant of this collapse which holds without built-in arithmetic. Finally, we relate these results to an open question regarding the expressive power of finite leaf automata with context-free leaf languages.

We study definability of second order generalized quantifiers on finite structures. Our main result says that for every second order type t there exists a second order generalized quantifier of type t which is not definable in the extension of second order logic by all second order generalized quantifiers of types lower than t.

A correction is needed for the singular case X = ∅ in Theorems 4.9, 4.10, 5.1, and 5.2. In Kontinen and Vaananen (2009), the open formulas of Dependence Logic (D) were studied. Formulas of dependence logic express properties of sets of assignments (teams). It was shown in Vaananen (2007) that every formula of dependence logic can be represented in an equivalent form in existential second-order logic ( 1 1) with an extra predicate, occurring only negatively, interpreting the team. In Theorems 4.9 and 4.10 of Kontinen and Vaananen (2009) it was claimed that also the converse holds, i.e., that for every vocabulary L and sentence φ ∈ 1 1[L ∪ {R}], in which R is k-ary (for some k ≥ 1) and occurs only negatively, there is a formula ψ(y1, . . . , yk) ∈ D[L] such that for all models A and teams X with domain {y1, . . . , yk} A | X ψ ⇔ (A, rel(X)) | φ, (1)

Proceeding volume: 46 Inclusion dependencies are one of the most important database constraints. In isolation their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. In contrast, finite and unrestricted implication problems for the combined class of functional and inclusion de- pendencies deviate from one another and are each undecidable. The same holds true for the class of embedded multivalued dependencies. An important embedded tractable fragment of embedded multivalued dependencies are independence atoms. These stipulate independence between two attribute sets in the sense that for every two tuples there is a third tuple that agrees with the first tuple on the first attribute set and with the second tuple on the second attribute set. For independence atoms, their finite and unrestricted implication problems coincide, are finitely axiomatizable, and decidable in cubic time. In this article, we study the implication problems of the combined class of independence atoms and inclusion dependencies. We show that their finite and unrestricted implication problems coincide, are finitely axiomatizable, PSPACE-complete, and fixed-parameter tractable in their arity. Hence, significant expressivity is gained without sacrificing any of the desirable properties that inclusion dependencies have in isolation. Finally, we establish an efficient condition that is sufficient for independence atoms and inclusion dependencies not to inter- act. The condition ensures that we can apply known algorithms for deciding implication of the individual classes of independence atoms and inclusion dependencies, respectively, to decide implication for an input that combines both individual classes.

Team logic is a new logic, introduced by Vaananen [1], extending dependence logic by classical negation. Dependence logic adds to first-order logic atomic formulas expressing functional dependence of variables on each other. It is known that on the level of sentences dependence logic and team logic are equivalent with existential second-order logic and full second-order logic, respectively. In this article we show that, in a sense that we make explicit, team logic and second-order logic are also equivalent with respect to open formulas. A similar earlier result relating open formulas of dependence logic to the negative fragment of existential second-order logic was proved in [2].