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.

We characterise the computational power of recurrent graph neural networks (GNNs) in terms of arithmetic circuits over the real numbers. Our networks are not restricted to aggregate-combine GNNs or other particular types. Generalising similar notions from the literature, we introduce the model of recurrent arithmetic circuits, which can be seen as arithmetic analogues of sequential or logical circuits. These circuits utilise so-called memory gates which are used to store data between iterations of the recurrent circuit. While (recurrent) GNNs work on labelled graphs, we construct arithmetic circuits that obtain encoded labelled graphs as real valued tuples and then compute the same function. For the other direction we construct recurrent GNNs which are able to simulate the computations of recurrent circuits. These GNNs are given the circuit-input as initial feature vectors and then, after the GNN-computation, have the circuit-output among the feature vectors of its nodes. In this way we establish an exact correspondence between the expressivity of recurrent GNNs and recurrent arithmetic circuits operating over real numbers. Our results both deepen our understanding of the capabilities of trained neural networks and open new approaches to study recurrent neural networks using the lens of circuit complexity theory.

Abstract In the eighties, Immerman showed that the class of languages definable by first-order formulae coincides with the class of languages decidable by unbounded fan-in Boolean circuits of constant depth and polynomial size. We show an analogous result for real-valued computation, i.e. we define circuits of unbounded fan-in operating over real numbers and show that families of such circuits of polynomial size and constant depth decide exactly those sets of vectors of reals that can be defined in first-order logic on real valued structures. Our characterization holds both non-uniformly as well as for many natural uniformity conditions.

We characterize the computational power of neural networks that follow the graph neural network (GNN) architecture, not restricted to aggregate-combine GNNs or other particular types. We establish an exact correspondence between the expressivity of GNNs using diverse activation functions and arithmetic circuits over real numbers. In our results the activation function of the network becomes a gate type in the circuit. Our result holds for families of constant depth circuits and networks, both uniformly and non-uniformly, for all common activation functions.

Abstract We present an adapted construction of algebraic circuits over the reals introduced by Cucker and Meer to arbitrary infinite integral domains and generalize the $\mathrm{AC}_{\mathbb{R}}$ and $\mathrm{NC}_{\mathbb{R}}^{}$ classes for this setting. We give a theorem in the style of Immerman’s theorem which shows that for these adapted formalisms, sets decided by circuits of constant depth and polynomial size are the same as sets definable by a suitable adaptation of first-order logic. Additionally, we discuss a generalization of the guarded predicative logic by Durand, Haak and Vollmer, and we show characterizations for the $\mathrm{AC}_{R}$ and $\mathrm{NC}_R^{}$ hierarchy. Those generalizations apply to the Boolean $\mathrm{AC}$ and $\mathrm{NC}$ hierarchies as well. Furthermore, we introduce a formalism to be able to compare some of the aforementioned complexity classes with different underlying integral domains.

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.