AlMoTh 2022

Benedikt Pago

Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus.

We extend prior work on the connections between logics from finite model theory and propositional/algebraic proof systems. We show that if all non-isomorphic graphs in a given graph class can be distinguished in the logic Choiceless Polynomial Time with counting (CPT), then they can also be distinguished in the bounded-degree extended polynomial calculus (EPC), and the refutations have roughly the same size as the resource consumption of the CPT-sentence. This allows to transfer lower bounds for EPC to CPT and thus constitutes a new potential approach towards understanding the limits of CPT. A super-polynomial EPC lower bound for a PTIME-instance of the graph isomorphism problem would separate CPT from P and thus solve a major open question in finite model theory. Further, our result yields a model theoretic proof for the separation of the bounded-degree polynomial calculus from the bounded-degree extended polynomial calculus.

Matthias Naaf

Fixed-Point Logic with Semiring Semantics: How to Compute Greatest Fixed Points

We discuss the algorithmic evaluation of formulae in least fixed-point logic LFP under semiring semantics, which generalises Boolean semantics by replacing truth values with values from a commutative semiring. These values can represent information such as confidence or costs, and can also be used for provenance analysis of games with fixed-point objectives, such as Büchi games. The evaluation of LFP-formulae (in a given structure with semiring annotations) then requires the computation of fixed points over semirings, which is non-trivial for infinite semirings. We show that in absorptive semirings (with certain completeness assumptions), both least and greatest fixed points of polynomial systems, such as the ones induced by LFP-formulae, can be computed in a polynomial number of semiring operations.

Tim Seppelt

Homomorphism Tensors and Linear Equations

Lovász (1967) showed that two graphs $G$ and $H$ are isomorphic if and only if they are homomorphism indistinguishable over the class of all graphs, i.e. for every graph $F$, the number of homomorphisms from $F$ to $G$ equals the number of homomorphisms from $F$ to $H$. Recently, homomorphism indistinguishability over restricted classes of graphs such as bounded treewidth, bounded treedepth and planar graphs, has emerged as a surprisingly powerful framework for capturing diverse equivalence relations on graphs arising from logical equivalence and algebraic equation systems.

In this talk, a unified algebraic framework for such results is introduced by examining the linear-algebraic and representation-theoretic structure of tensors counting homomorphisms from labelled graphs. The existence of certain linear transformations between such homomorphism tensor subspaces can be interpreted both as homomorphism indistinguishability over a graph class and as feasibility of an equational system.

This is joint work with Martin Grohe and Gaurav Rattan.

Erich Gr?del

Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics

Semiring semantics evaluates logical statements not just to true or false, but to values in some commutative semiring.

As part of a general project to study the (finite) model theory of semiring semantics, we consider here random semiring interpretations, induced by a probability distribution on a (finite or infinite) semiring, and we investigate here the question of how classical results on first-order logic on random structures, most importantly the 0-1 law,  generalise to semiring semantics.

It is an immediate consequence of the classical 0-1 law that a first-order sentence is, asymptotically, either almost surely evaluated to 0 by random semiring interpretations, or almost surely takes only values different from 0. However, by means of a more sophisticated  analysis, based on appropriate extension properties and on algebraic representations of  first-order formulae by polynomials, we can prove stronger results.

For many semirings, FO can be partitioned into classes F(j), such that every sentence in F(j)  evaluates almost surely to j under random semiring interpretations. Further, for most of the  semirings studied here, this partition actually collapses to just three classes F(0), F(1), and F(e), of sentences that, respectively, almost surely evaluate to 0, 1, and to the infimum e of all non-zero  values of the semiring. For all other values j in the semiring we have that F(j) is empty.

A semiring where the analysis is somewhat different is the natural semiring (N,+,*,0,1) for which multiplication is increasing rather than decreasing with respect to the natural semiring order.

This is joint work with Hayyan Helal, Matthias Naaf, and Richard Wilke. 

Moritz Lichter

Extending Choiceless Polynomial Time with Choices

Choiceless Polynomial Time (CPT) is the currently only remaining promising candidate in the quest for a logic capturing PTime. We extend CPT with a choice operator allowing choices from definable orbits. To ensure polynomial time evaluation, automorphisms have to be provided to certify that the choice set is indeed an orbit.

For the resulting logic we show that for every class of structures for which isomorphism is definable, the logic automatically captures PTime. To do so we argue that, in this logic, definable isomorphism implies definable canonization.

Thereby, our construction removes the non-trivial step of extending isomorphism definability results to canonization. This step was a part of proofs that show that CPT or other logics capture PTime on a particular class of structures. The step typically required substantial extra effort.

Max Merz

Probabilistic Databases under Updates: Boolean Query Evaluation and Ranked Enumeration
 

This talk will be about query evaluation on tuple-independent probabilistic databases in a dynamic setting, where tuples can be inserted or deleted. In this context we are interested in efficient data structures for maintaining the query result of Boolean as well as non-Boolean queries.
For Boolean queries, we show how the known lifted inference rules can be made dynamic, so that they support single-tuple updates with only a constant number of arithmetic operations. As a consequence, we obtain that the probability of every safe UCQ can be maintained with constant update time.
For non-Boolean queries, our task is to enumerate all result tuples ranked by their probability. We develop lifted inference rules for non-Boolean queries, and, based on these rules, provide a dynamic data structure that allows both log-time updates and ranked enumeration with logarithmic delay. As an application, we identify a fragment of non-repeating conjunctive queries that supports log-time updates as well as log-delay ranked enumeration. This characterisation is tight under the OMv-conjecture.
This is joint work with Christoph Berkholz.

Florian Bruse

A Decidable Non-Regular Modal Fixpoint Logic

Fixpoint Logic with Chop (FLC) extends the modal $\mu$-calculus with an operator for sequential composition between predicate transformers. This makes it an expressive modal fixpoint logic which is capable of formalising many non-regular program properties. Its satisfiability problem is highly undecidable. Here we define Visibly Pushdown Fixpoint Logic with Chop (vpFLC), a fragment in which fixpoint formulas are required to be of a certain form resembling visibly pushdown grammars. We give a sound and complete game-theoretic characterisation of FLC's satisfiability problem and show that the games corresponding to formulas from vpFLC are stair-parity games and therefore effectively solvable, resulting in 2-EXPTIME-completeness of this fragment. The lower bound is inherited from PDL over Recursive Programs, which is structurally similar but considerably weaker in expressive power.
This is joint work with Martin Lange.

Nicole Schirrmacher

Separator logic and disjoint-paths logic

Separator logic FO+conn and disjoint-paths logic FO+DP are extensions of first-order logic FO by connectivity predicates conn_k and disjoint-paths predicates disjoint-paths_k. We study the expressive power of these logics and their model-checking problem. Separator logic can express e.g. acyclicity, k-connectivity, and elimination distance problems to first-order definition classes. Its model-checking problem is fixed-parameter tractable on classes of graphs with excluded topological minor. Disjoint-paths logic can additionally express e.g. the disjoint-paths problem, the existence of (topological) minor, and planarity.
This is joint work with Sebastian Siebertz and Alexandre Vigny.

Marko Schmellenkamp

Iltis: Learning Logic in the Web

The Iltis project provides an interactive, web-based system for teaching the foundations of formal methods. It is designed with the objective to allow for simple inclusion of new educational tasks; to pipeline such tasks into more complex exercises; and to allow simple inclusion and cascading of feedback mechanisms. Currently, exercises for many typical automated reasoning workflows for propositional logic, modal logic, and some parts of first-order logic are covered.
In this talk I will address (algorithmic) challenges and solution approaches for building such systems, but also show how the system can be used in logic instruction.

Alexandre Vigny

Discrepancy and Sparsity

Discrepancy is a measure of the intricacy of a set system. A prime example of a set system are families of sets that are definable in a graph (using e.g. FO formulas). For example, the family of all neighborhoods, or all 2-hop neighborhoods. We show strong connections between the discrepancy of definable set systems and sparsity notions of graph classes such as: bounded degeneracy, bounded expansion, and nowhere dense.
These results where obtained in collaboration with Mario Grobler, Yiting Jiang, Patrice Ossona de Mendez, and Sebastian Siebertz.

Nikolas M?hlmann

Indiscernible sequences in monadically stable and monadically NIP classes

An indiscernible sequence in a structure is a sequence of elements which is very homogeneous in the sense that any two finite sub-sequences of the same length satisfy the same first-order formulas. We provide new characterizations of monadically stable and monadically NIP classes of structures in terms of indiscernible sequences by showing that they impose a strongstructure on their  neighborhoods. From their study we derive several interesting combinatorial and algorithmic properties of monadically stable classes of finite graphs.

Christoph Standke

Probabilistic Query Evaluation with Bag Semantics

Probabilistic databases (PDBs) are usually introduced as probability spaces over the subsets of a finite set of possible facts. Probabilistic query evaluation (PQE) is the problem of finding the probability that a Boolean query evaluates to true on a given PDB. The data complexity of PQE is well-understood for the classof unions of conjunctive queries on tuple-independent PDBs: for every query, the problem can be classified to be either solvable in polynomial time, or is #P-hard (Dalvi & Suciu, JACM 2012).
In this talk, we discuss a version of PQE, where both the query evaluation, and the probabilistic databases use a bag semantics. That is, the input PDB may contain duplicates, and the query evaluation takes tuple multiplicities into account. Our main focus lies on self-join free conjunctive queries, where we obtain a dichotomy similar to the one above. This is achieved by combining known results for the set version of the problem with novel techniques that are required to handle distributions over multiplicities. This is joint work with Martin Grohe and Christoph Standke.