AlMoTh 2022

AlMoTh 2022

The AlMoTh 2022 meeting will take place in Bremen, on Monday/Tuesday, March 21rst and 22nd.

For registration please send an email to almoth[at]uni-bremen[dot]de If you are interested to give a talk, please add title and abstract.

Programm

Monday
12:00-13:30 Welcome Soup
13:30-18:00 Presentations
19:30 Dinner

Tuesday
9:00-13:00 Presentations

Venue: Cartesium
Enrique-Schmidt-Strasse,
28359 Bremen, Germany

Public transportation stop
Streetcar: Universität-Süd
Bus: Universität-Süd

Monday 21.3.

13:45 - 14:15
Erich Grädel: Zero-One Laws and Almost Sure Valuations of First-Order Logic in Semiring Semantics

14:15 - 14:45
Matthias Naaf: Fixed-Point Logic with Semiring Semantics: How to Compute Greatest Fixed Points

14:45 - 15:15
Florian Bruse: A Decidable Non-Regular Modal Fixpoint Logic

15:15 - 15:45 Coffee Break

15:45 - 16:15
Sarah Kleest-Meißner: Discovering Event Queries from Traces: Laying Foundations for Subsequence-Queries with Wildcards and Gap-Size Constraints

16:15 - 16:45
Max Merz: Probabilistic Databases under Updates: Boolean Query Evaluation and Ranked Enumeration

16:45 - 17:00 Short Break

17:00 - 17:30
Christoph Standke: Probabilistic Query Evaluation with Bag Semantics

17:30 - 18:00
Alexandre Vigny: Discrepancy and Sparsity

Tuesday

9:00 - 9:30
Benedikt Pago: Distinguishing graphs in Choiceless Polynomial Time and the Extended Polynomial Calculus.

9:30 - 10:00
Moritz Lichter: Extending Choiceless Polynomial Time with Choices

10:00 - 10:30
Nicole Schirrmacher: Separator logic and disjoint-paths logic

10:30 - 11:00 Coffee Break

11:00 - 11:30

11:30 - 12:00
Marko Schmellenkamp: Iltis: Learning Logic in the Web

12:00 - 12:30
Tim Seppelt. Homomorphism Tensors and Linear Equations

Sarah Kleest-Meißner

Discovering Event Queries from Traces: Laying Foundations for Subsequence-Queries with Wildcards and Gap-Size Constraints

We introduce subsequence-queries with wildcards and gap-size constraints (swg-queries, for short) as a tool for querying event traces. An swg-query q is given by a string s over an alphabet of variables and types, a global window size w and a tuple c = ((c_1^-,c_1^+),(c_2^-,c_2^+), ..., (c_(|s|-1)^-, c_(|s|-1)^+)) of local gap-size constraints. The query q matches in a trace t (i.e., a sequence of types) if the variables can uniformly be substituted by types such that the resulting string occurs in t as a subsequence that spans an area of length at most w, and the i-th gap of  the subsequence (i. e., the distance between the i-th and (i+1)-th position of the subsequence) has length at least  c_i^- and at most c_i+.
We formalise and investigate the task of discovering an swg-query that describes best the traces from a given sample S of traces, and we present an algorithm solving this task. As a central component, our algorithm repeatedly solves the matching problem (i.e., deciding whether a given query q matches in a given trace t), which is an NP-complete problem (in combined complexity). Hence, the matching problem is of special interest in the context of query discovery, and we therefore subject it to a detailed (parameterised) complexity analysis to identify tractable subclasses, which lead to tractable subclasses of the discovery problem as well. We complement this by a reduction proving that any query discovery algorithm also yields an algorithm for the matching problem. Hence, lower bounds on the complexity of the matching problem directly translate into according lower bounds of the query discovery problem.

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.