Michael Benedikt

We overview applications of Craig interpolation and Beth definability to simplifying logical expressions or database queries. From the perspective of the theory of interpolation and definability the results give a number of new angles. First, they give a different take on what it means to make definability or interpolation results effective, looking at algorithms that take a proof as input and return an interpolant or explicit definition as output. Secondly, they relate interpolation and definability to preservation theorems in model theory: interpolation and definability theorems are the basis for many “semantics-to-syntax” results, relating a semantic property of a formula to its equivalence with a certain syntactic form. Thirdly, they motivate new forms of interpolation and definability, focusing on syntactic forms that are of interest in databases.

We present results concerning the expressiveness and decidability of a popular graph learning formalism, graph neural networks (GNNs), exploiting connections with logic. We use a family of recently-discovered decidable logics involving “Presburger quantifiers.” We show how to use these logics to measure the expressiveness of classes of GNNs, in some cases getting exact correspondences between the expressiveness of logics and GNNs. We also employ the logics, and the techniques used to analyze them, to obtain decision procedures for verification problems over GNNs. We complement this with undecidability results for static analysis problems involving the logics, as well as for GNN verification problems.

We revisit evaluation of logical formulas that allow both uninterpreted relations, constrained to be finite, as well as an interpreted vocabulary over an infinite domain. This formalism was denoted embedded finite model theory in the past. It is clear that the expressiveness and evaluating complexity of formulas of this type depend heavily on the infinite structure. If we embed in a wild structure like the integers with additive and multiplicative arithmetic, logic is extremely expressive and formulas are impossible to evaluate. On the other hand, for some well-known decidable structures, the expressiveness and evaluating complexity are similar to the situation without the additional infrastructure. The latter phenomenon was formalized via the notion of “Restricted Quantifier Collapse”: adding quantification over the infinite structure does not add expressiveness. Beyond these two extremes little was known. In this work we show that the possibilities for expressiveness and complexity are much wider. We show that we can get almost any possible complexity of evaluation while staying within a decidable structure. We also show that in some decidable structures, there is a disconnect between expressiveness of the logic and complexity, in that we cannot eliminate quantification over the structure, but this is not due to an ability to embed complex relational computation in the logic. We show failure of collapse for the theory of finite fields and the related theory of pseudo-finite fields, which will involve coding computation in the logic. As a by-product of this, we establish the first lower bounds for the complexity of decision procedures for several decidable theories of fields, including the theory of finite fields. This article includes material in the extended abstract “Embedded Finite Models: Beyond Restricted Quantifier Collapse,” that appeared in the Logic in Computer Science conference (LICS ’23).

Graph neural networks (GNNs) are a widely used class of machine learning models for graph-structured data, based on local aggregation over neighbors. GNNs have close connections to logic. In particular, their expressive power is linked to that of modal logics and bounded-variable logics with counting. In many practical scenarios, graphs processed by GNNs have node features that act as unique identifiers. In this work, we study how such identifiers affect the expressive power of GNNs. We initiate a study of the key-invariant expressive power of GNNs, inspired by the notion of order-invariant definability in finite model theory: which node queries that depend only on the underlying graph structure can GNNs express on graphs with unique node identifiers? We provide answers for various classes of GNNs with local max- or sum-aggregation.

We investigate multi-label classification involving large sets of labels, where the output labels may be known to satisfy some logical constraints. We look at an architecture in which classifiers for individual labels are fed into an expressive sequential model, which produces a joint distribution. One of the potential advantages for such an expressive model is its ability to modelling correlations, as can arise from constraints. We empirically demonstrate the ability of the architecture both to exploit constraints in training and to enforce constraints at inference time.

Guarded tuple-generating dependencies (GTGDs) are a natural extension of description logics and referential constraints. It has long been known that queries over GTGDs can be answered by a variant of the chase —a quintessential technique for reasoning with dependencies. However, there has been little work on concrete algorithms and even less on implementation. To address this gap, we revisit Datalog rewriting approaches to query answering, where a set of GTGDs is transformed to a Datalog program that entails the same base facts on each base instance. We show that a rewriting consists of “shortcut” rules that circumvent certain chase steps, we present several algorithms that compute a rewriting by deriving such “shortcuts” efficiently, and we discuss important implementation issues. Finally, we show empirically that our techniques can process complex GTGDs derived from synthetic and real benchmarks and are thus suitable for practical use.

Derived datasets can be defined implicitly or explicitly. An implicit definition (of dataset O in terms of datasets I) is a logical specification involving two distinguished sets of relational symbols. One set of relations is for the "source data" I, and the other is for the "interface data" O. Such a specification is a valid definition of O in terms of I, if any two models of the specification agreeing on I agree on O. In contrast, an explicit definition is a transformation (or "query" below) that produces O from I. Variants of Beth's theorem state that one can convert implicit definitions to explicit ones. Further, this conversion can be done effectively given a proof witnessing implicit definability in a suitable proof system. We prove the analogous implicit-to-explicit result for nested relations: implicit definitions, given in the natural logic for nested relations, can be converted to explicit definitions in the nested relational calculus (NRC). We first provide a model-theoretic argument for this result, which makes some additional connections that may be of independent interest, between NRC queries, interpretations, a standard mechanism for defining structure-to-structure translation in logic, and between interpretations and implicit to definability "up to unique isomorphism". The latter connection uses a variation of a result of Gaifman concerning "relatively categorical" theories. We also provide a proof-theoretic result that provides an effective argument: from a proof witnessing implicit definability, we can efficiently produce an NRC definition. This will involve introducing the appropriate proof system for reasoning with nested sets, along with some auxiliary Beth-type results for this system. As a consequence, we can effectively extract rewritings of NRC queries in terms of NRC views, given a proof witnessing that the query is determined by the views.

We consider the extension of [Formula: see text] with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence, i.e., the set of the sizes of its finite models, is definable in Presburger arithmetic. In the process we present several refinements to the “biregular graph method.” In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.

We consider the extension of two variable logic with quantifiers that state that the number of elements where a formula holds should belong to a given ultimately periodic set. We show that both satisfiability and finite satisfiability of the logic are decidable. We also show that the spectrum of any sentence is definable in Presburger arithmetic. In the process we present several refinements to the ``biregular graph method''. In this method, decidability issues concerning two-variable logics are reduced to questions about Presburger definability of integer vectors associated with partitioned graphs, where nodes in a partition satisfy certain constraints on their in- and out-degrees.