We study the expressive power and computational properties of first-order logic and its extensions under the semiring semantics originating from the seminal work of Green, Karvounarakis, and Tannen. While semiring semantics is currently extensively used, e.g., in the study of provenance in database theory and description logic, a comprehensive computational analysis of these logics acting over general semirings is still lacking. We analyse expressivity, and complexity of model-checking of first-order formulas in this framework, providing characterizations in terms of generalized Blum–Shub–Smale machines over semirings. We also show a variant of Fagin's theorem, i.e., a logical characterization of nondeterministic polynomial time over semirings using a version of existential second-order logic. We further generalize Cook's theorem for the semiring framework and show that propositional satisfiability in the semiring semantics is complete for this notion of NP, and that the true existential first-order theory of the semiring is complete for its Boolean fragment.

This paper establishes and proves representation theorems for cumulative propositional dependence logic and for cumulative propositional logic with team semantics. Cumulative logics are famously given by System~C. For propositional dependence logic, we show that System C entailments are exactly captured by cumulative models from Kraus, Lehmann and Magidor. On the other hand, we show that entailment in cumulative propositional logics with team semantics is exactly captured by cumulative and asymmetric models. For the latter, we also obtain equivalence with cumulative logics based on propositional logic with classical semantics. The proofs will be useful for proving representation theorems for other cumulative logics without negation and material implication.

Abstract Linear temporal logic (LTL) is used in system verification to write formal specifications for reactive systems. However, some relevant properties, e.g. non-inference in information flow security, cannot be expressed in LTL. A class of such properties that has recently received ample attention is known as hyperproperties. There are two major streams in the research regarding capturing hyperproperties, namely hyperlogics, which extend LTL with trace quantifiers (HyperLTL), and logics that employ team semantics, extending truth to sets of traces. In this article we explore the relation between asynchronous LTL under set-based team semantics (TeamLTL) and HyperLTL. In particular we consider the extensions of TeamLTL with the Boolean disjunction and a fragment of the extension of TeamLTL with the Boolean negation, where the negation cannot occur in the right-hand side of the strong release operator or within the global operator. We show that TeamLTL extended with the Boolean disjunction is equi-expressive with the positive Boolean closure of HyperLTL restricted to one universal quantifier, while the right-downward closed fragment of TeamLTL extended with the Boolean negation is expressively equivalent with the Boolean closure of HyperLTL restricted to one universal quantifier. Furthermore, we show that formulae of TeamLTL extended with the Boolean negation are equivalent with sentences of first-order logic interpreted over grid structures.

Implicit computational complexity is a lively area of theoretical computer science, which aims to provide machine-independent characterizations of relevant complexity classes. One of the seminal works in this field appeared in the 1960s, when Cobham introduced a function algebra closed under bounded recursion on notation to capture polynomial time computable functions ( FP ). Later on, several complexity classes have been characterized using limited recursion schemas. In this context, an original approach has been recently introduced, showing that ordinary differential equations (ODEs) offer a natural tool for algorithmic design and providing a characterization of FP by a new ODE-schema. In the present paper we generalize this approach by presenting original ODE-characterizations for the small circuit classes FAC 0 and FTC 0 .

This paper considers the complexity and properties of KLM-style preferential reasoning in the setting of propositional logic with team semantics and dependence atoms, also known as propositional dependence logic. Preferential team-based reasoning is shown to be cumulative, yet violates System P. We give intuitive conditions that fully characterise those cases where preferential propositional dependence logic satisfies System P. We show that these characterisations do, surprisingly, not carry over to preferential team-based propositional logic. Furthermore, we show how classical entailment and dependence logic entailment can be expressed in terms of non-trivial preferential models. Finally, we present the complexity of preferential team-based reasoning for two natural representations. This includes novel complexity results for classical (non-team-based) preferential reasoning.

In this paper, we provide a uniform framework for investigating small circuit classes and bounds through the lens of ordinary differential equations (ODEs). Following an approach recently introduced to capture the class of polynomial-time computable functions via ODE-based recursion schemas and later applied to the context of functions computed by unbounded fan-in circuits of constant depth (FAC⁰), we study multiple relevant small circuit classes. In particular, we show that natural restrictions on linearity and derivation along functions with specific growth rate correspond to kinds of functions that can be proved to be in various classes, ranging from FAC⁰ to FAC¹. This reveals an intriguing link between constraints over linear-length ODEs and circuit computation, providing new tools to tackle the complex challenge of establishing bounds for classes in the circuit hierarchies and possibly enhancing our understanding of the role of counters in this setting. Additionally, we establish several completeness results, in particular obtaining the first ODE-based characterizations for the classes of functions computable in constant depth with unbounded fan-in and Mod 2 gates (FACC[2]) and in logarithmic depth with bounded fan-in Boolean gates (FNC¹).

We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We relate the new semantics with the original semantics based on multisets and establish one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics.

Abstract We study the expressivity and the complexity of various logics in probabilistic team semantics with the Boolean negation. In particular, we study the extension of probabilistic independence logic with the Boolean negation, and a recently introduced logic first-order theory of random variables with probabilistic independence. We give several results that compare the expressivity of these logics with the most studied logics in probabilistic team semantics setting, as well as relating their expressivity to a numerical variant of second-order logic. In addition, we introduce novel entropy atoms and show that the extension of first-order logic by entropy atoms subsumes probabilistic independence logic. Finally, we obtain some results on the complexity of model checking, validity and satisfiability of our logics.

In this article, we consider the interplay of generalized quantifiers and built-in relations over finite structures, in particular, in the range of logics capturing the circuit complexity classes \(\mathrm{AC^{0}}\) and \(\mathrm{TC^{0}}\) . It is well known that for capturing \(\mathrm{AC^{0}}\) first-order logic has to be equipped with order and, e.g., predicates for addition and multiplication, whereas for \(\mathrm{TC^{0}}\) generalized quantifiers such as majority quantifiers are necessary. The sharp division between the classes \(\mathrm{AC^{0}}\) and \(\mathrm{TC^{0}}\) can be explained by the fact that \(\mathrm{AC^{0}}\) is not closed under restricting \(\mathrm{AC^{0}}\) -computable queries into simple subsequences of the input, whereas \(\mathrm{TC^{0}}\) is closed under such relativization as its queries can be expressed in terms of first-order formulas using universe-independent generalized quantifiers and order as the only built-in relation. In the terminology of abstract logics, the above means that logics capturing \(\mathrm{AC^{0}}\) do not have the relativization property, and hence, they are not regular logics unlike the logics capturing \(\mathrm{TC^{0}}\) . This weakness of \(\mathrm{AC^{0}}\) has been also elaborated in the line of research on the Crane Beach Conjecture. The conjecture (which was refuted by Barrington et al.) was that if a language \( L \) has a neutral letter, then \( L \) can be defined in \(\operatorname{FO}_{\mathcal{A}}\) , first-order logic with the collection of all numerical built-in relations \(\mathcal{A}\) , if and only if \( L \) can be already defined in \(\operatorname{FO}_{\leq}\) . Our approach is two-fold. First, we study universe-independent cardinality quantifiers \(\operatorname{\mathsf{Q}}\) defined by a parameter set \(S\subseteq\mathbb{N}\) and formulate a combinatorial criterion for \( S \) implying that all languages in \(\mathrm{DLOGTIME}\) -uniform \(\mathrm{TC^{0}}\) can be defined in \(\operatorname{FO}_{\leq}(\operatorname{\mathsf{Q}})\) . For instance, this criterion is satisfied if \( S \) is the range of some polynomial with positive integer coefficients of degree at least two. Second, by adapting the key properties of abstract logics to accommodate built-in relations, we define the regular interior \(\operatorname{\mathcal{R}-int}(\mathcal{L})\) (the largest regular \(\mathcal{L}^{*}\) such that \(\mathcal{L}^{*}\subseteq\mathcal{L}\) ) and regular closure \(\operatorname{\mathcal{R}-cl}(\mathcal{L})\) (the least regular \(\mathcal{L}^{*}\) such that \(\mathcal{L}\subseteq\mathcal{L}^{*}\) ), of a logic \(\mathcal{L}\) with built-in relations, and show that the Crane Beach Conjecture can be interpreted as a statement concerning the regular interior of \(\mathcal{L}\) . By extending the results of Barrington et al., we further show that if \(\mathcal{B}=\{+\}\) , or \(\mathcal{B}\) contains only unary relations besides \(\leq\) , then \(\operatorname{\mathcal{R}-int}(\operatorname{FO}_{\mathcal{B}})\equiv \operatorname{FO}_{\leq}\)

The training problem of neural networks (NNs) is known to be ER-complete with respect to ReLU and linear activation functions. We show that the training problem for NNs equipped with arbitrary activation functions is polynomial-time bireducible to the existential theory of the reals extended with the corresponding activation functions. For effectively continuous activation functions (e.g., the sigmoid function), we obtain an inclusion to low levels of the arithmetical hierarchy. Consequently, the sigmoid activation function leads to the existential theory of the reals with the exponential function, and hence the decidability of training NNs using the sigmoid activation function is equivalent to the decidability of the existential theory of the reals with the exponential function, a long-standing open problem. In contrast, we obtain that the training problem is undecidable if sinusoidal activation functions are considered.

Implicit computational complexity is an active area of theoretical computer science, which aims at providing machine-independent characterizations of relevant complexity classes. One of the seminal works in this field appeared in 1965, when Cobham introduced a function algebra closed under bounded recursion on notation to capture FP. Later on, several complexity classes have been characterized using limited recursion schemas. In this context, a new approach was recently introduced, showing that ordinary differential equations (ODEs) offer a natural tool for algorithmic design and providing a characterization of FP by an ODE-schema. The overall goal of the present work is precisely that of generalizing this approach to parallel computation, obtaining an original ODE-characterization for the small circuit classes FAC⁰ and FTC⁰.

We study the complexity of reasoning tasks for logics in team semantics. Our main focus is on the data complexity of model checking but we also derive new results for logically defined counting and enumeration problems. Our approach is based on modular reductions of these problems into the corresponding problems of various classes of Boolean formulas. We illustrate our approach via several new tractability/intractability results.

Abstract In this article, we study the complexity of weighted team definability for logics with team semantics. This problem is a natural analog of one of the most studied problems in parameterized complexity, the notion of weighted Fagin-definability, which is formulated in terms of satisfaction of first-order formulas with free relation variables. We focus on the parameterized complexity of weighted team definability for a fixed formula $\varphi$ of central team-based logics. Given a first-order structure $\mathcal{A}$ and the parameter value $k\in \mathbb N$ as input, the question is to determine whether $\mathcal{A},T\models \varphi$ for some team T of size k. We show several results on the complexity of this problem for dependence, independence, and inclusion logic formulas. Moreover, we also relate the complexity of weighted team definability to the complexity classes in the well-known W-hierarchy as well as paraNP.

Semiring semantics for first-order logic provides a way to trace how facts represented by a model are used to deduce satisfaction of a formula. Team semantics is a framework for studying logics of dependence and independence in diverse contexts such as databases, quantum mechanics, and statistics by extending first-order logic with atoms that describe dependencies between variables. Combining these two, we propose a unifying approach for analysing the concepts of dependence and independence via a novel semiring team semantics, which subsumes all the previously considered variants for first-order team semantics. In particular, we study the preservation of satisfaction of dependencies and formulae between different semirings. In addition we create links to reasoning tasks such as provenance, counting, and repairs.

We introduce and develop a set-based semantics for asynchronous TeamLTL. We consider two canonical logics in this setting: the extensions of TeamLTL by the Boolean disjunction and by the Boolean negation. We establish fascinating connections between the original semantics based on multisets and the new set-based semantics as well as show one of the first positive complexity theoretic results in the temporal team semantics setting. In particular we show that both logics enjoy normal forms that can be utilised to obtain results related to expressivity and complexity (decidability) of the new logics. We also relate and apply our results to recently defined logics whose asynchronicity is formalized via time evaluation functions.

Abstract In this paper, we introduce a logic based on team semantics, called $\mathbf {FOT} $ , whose expressive power is elementary, i.e., coincides with first-order logic both on the level of sentences and (possibly open) formulas, and we also show that a sublogic of $\mathbf {FOT} $ , called $\mathbf {FOT}^{\downarrow } $ , captures exactly downward closed elementary (or 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 define and study logics in the framework of probabilistic team semantics and over metafinite structures. Our work is paralleled by the recent development of novel axiomatizable and tractable logics in team semantics that are closed under the Boolean negation. Our logics employ new probabilistic atoms that resemble so-called extended atoms from the team semantics literature. We also define counterparts of our logics over metafinite structures and show that all of our logics can be translated into functional fixed point logic implying a polynomial time upper bound for data complexity with respect to BSS-computations.

Abstract In this paper, we investigate the parameterized complexity of model checking for Dependence and Independence logic, which are well studied logics in the area of Team Semantics. We start with a list of nine immediate parameterizations for this problem, namely the number of disjunctions (i.e. splits)/(free) variables/universal quantifiers, formula-size, the tree-width of the Gaifman graph of the input structure, the size of the universe/team and the arity of dependence atoms. We present a comprehensive picture of the parameterized complexity of model checking and obtain a division of the problem into tractable and various intractable degrees. Furthermore, we also consider the complexity of the most important variants (data and expression complexity) of the model checking problem by fixing parts of the input.

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.

We introduce a novel variant of BSS machines called Separate Branching BSS machines (S-BSS in short) and develop a Fagin-type logical characterisation for languages decidable in nondeterministic polynomial time by S-BSS machines. We show that NP on S-BSS machines is strictly included in NP on BSS machines and that every NP language on S-BSS machines is a countable disjoint union of closed sets in the usual topology of Rn. Moreover, we establish that on Boolean inputs NP on S-BSS machines without real constants characterises a natural fragment of the complexity class ∃R (a class of problems polynomial time reducible to the true existential theory of the reals) and hence lies between NP and PSPACE. Finally we apply our results to determine the data complexity of probabilistic independence logic.

Abstract Team semantics is the mathematical framework of modern logics of dependence and independence in which formulae are interpreted by sets of assignments (teams) instead of single assignments as in first-order logic. In order to deepen the fruitful interplay between team semantics and database dependency theory, we define Polyteam Semantics in which formulae are evaluated over a family of teams. We begin by defining a novel polyteam variant of dependence atoms and give a finite axiomatization for the associated implication problem. We relate polyteam semantics to team semantics and investigate in which cases logics over the former can be simulated by logics over the latter. We also characterize the expressive power of poly-dependence logic by properties of polyteams that are downwards closed and definable in existential second-order logic ($\textsf{ESO}$). The analogous result is shown to hold for poly-independence logic and all $\textsf{ESO}$-definable properties. We also relate poly-inclusion logic to greatest fixed point logic.

We study descriptive complexity of counting complexity classes in the range from #P to #*NP. A corollary of Fagin’s characterization of NP by existential second-order logic is that #P can be logically described as the class of functions counting satisfying assignments to free relation variables in first-order formulae. In this paper we extend this study to classes beyond #P and extensions of first-order logic with team semantics. These team-based logics are closely related to existential second-order logic and its fragments, hence our results also shed light on the complexity of counting for extensions of first-order logic in Tarski’s semantics. Our results show that the class #*NP can be logically characterized by independence logic and existential second-order logic, whereas dependence logic and inclusion logic give rise to subclasses of #*NP and #P, respectively. We also study the function class generated by inclusion logic and relate it to the complexity class TotP, which is a subclass of #P. Our main technical result shows that the problem of counting satisfying assignments for monotone Boolean Sigma_1-formulae is #*NP-complete with respect to Turing reductions as well as complete for the function class generated by dependence logic with respect to first-order reductions.

We classify the computational complexity of the satisfiability, validity, and model-checking problems for propositional independence, inclusion, and team logic. Our main result shows that the satisfiability and validity problems for propositional team logic are complete for alternating exponential-time with polynomially many alternations.

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 Semantics is a logical framework for the study of various dependency notions that are important in many areas of science. The starting point of this research is marked by the publication of the monograph Dependence Logic (Jouko Väänänen, 2007) in which first-order dependence logic is developed and studied. Since then team semantics has evolved into a flexible framework in which numerous logics have been studied. Much of the work in team semantics has so far focused on results concerning either axiomatic characterizations or the expressive power and computational aspects of various logics. This tutorial provides an introduction to team semantics with a focus on results regarding expressivity and computational aspects of the most prominent logics of the area. In particular, we discuss dependence, independence and inclusion logics in first-order, propositional, and modal team semantics. We show that first-order dependence and independence logic are equivalent with existential second-order logic and inclusion logic with greatest fixed point logic. In the propositional and modal settings we characterize the expressive power of these logics by so-called team bisimulations and determine the complexity of their model checking and satisfiability problems.

This article introduces modal independence logic MIL, a modal logic that can explicitly talk about independence among propositional variables. Formulas of MIL are not evaluated in worlds but in sets of worlds, so called teams. In this vein, MIL can be seen as a variant of Väänänen’s modal dependence logic MDL. We show that MIL embeds MDL and is strictly more expressive. However, on singleton teams, MIL is shown to be not more expressive than usual modal logic, but MIL is exponentially more succinct. Making use of a new form of bisimulation, we extend these expressivity results to modal logics extended by various generalized dependence atoms. We demonstrate the expressive power of MIL by giving a specification of the anonymity requirement of the dining cryptographers protocol in MIL. We also study complexity issues of MIL and show that, though it is more expressive, its satisfiability and model checking problem have the same complexity as for MDL.

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. We compare our classes with a hierarchy within #P defined in a model-theoretic way by Saluja et al. We 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 study the complexity of predicate logics based on team semantics. We show that the satisfiability problems of two-variable independence logic and inclusion logic are both NEXPTIME-complete. Furthermore, we show that the validity problem of two-variable dependence logic is undecidable, thereby solving an open problem from the team semantics literature. We also briefly analyse the complexity of the Bernays-Schoenfinkel-Ramsey prefix classes of dependence logic.

The famous van Benthem theorem states that modal logic corresponds exactly to the fragment of first-order logic that is invariant under bisimulation. In this article we prove an exact analogue of this theorem in the framework of modal dependence logic (MDL) and team semantics. We show that Modal Team Logic (MTL) extending MDL by classical negation captures exactly the FO-definable bisimulation invariant properties of Kripke structures and teams. We also compare the expressive power of MTL to most of the variants and extensions of MDL recently studied in the area.

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).

Uniqueness and independence are two fundamental properties of data. Their enforcement in knowledge systems can lead to higher quality data, faster data service response time, better data-driven decision making and knowledge discovery from data. The applications can be effectively unlocked by providing efficient solutions to the underlying implication problems of keys and independence atoms. Indeed, for the sole class of keys and the sole class of independence atoms the associated finite and general implication problems coincide and enjoy simple axiomatizations. However, the situation changes drastically when keys and independence atoms are combined. We show that the finite and the general implication problems are already different for keys and unary independence atoms. Furthermore, we establish a finite axiomatization for the general implication problem, and show that the finite implication problem does not enjoy a k-ary axiomatization for any k.

We study the expressive power of fragments of inclusion and independence logic defined either by restricting the number of universal quantifiers or the arity of inclusion and independence atoms in formulas. Assuming the so-called lax semantics for these logics, we relate these fragments of inclusion and independence logic to familiar sublogics of existential second-order logic. We also show that, with respect to the stronger strict semantics, inclusion logic is equivalent to existential second-order logic.

Abstract 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.

We study fragments D ( k ∀) and D ( k -dep) 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, for any fixed signature, the fragments D ( k ∀) give rise to an infinite hierarchy with respect to expressive power. On the other hand, for the fragments D ( k -dep), a hierarchy theorem is otained only in the case the signature is also allowed to vary. For any fixed signature, this question is open and is related to the so-called Spectrum Arity Hierarchy Conjecture.

We study the extension of dependence logic D by a majority quantifier 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, D(M) captures the complexity class counting hierarchy.

We study the two-variable fragments D2and IF2of dependence logic and independence-friendly logic. We consider the satisfiability and finite satisfiability problems of these logics and show that for D2, both problems are NEXPTIME-complete, whereas for IF2, the problems are undecidable. We also show that D2is strictly less expressive than IF2and that already in D2, equicardinality of two unary predicates and infinity can be expressed (the latter in the presence of a constant symbol).An extended version of this publication can be found at arxiv.org.

Team logic is a new logic, introduced by Väänänen [12], 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

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 quantifiersQkrinterpreted as “more than anr-fraction ofk-ary relations”. We show that the result holds for rational numbers of the forms/2mbut for any other 0 <r< 1 the corresponding logic satisfies the 0-1 law.

Abstract 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.