+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +**********************************************************************

Zeit: Freitag, 30. August 2024, 11:00 Uhr Ort: Raum 9222 (Informatikzentrum E3, Ahornstraße 55)

Referent: Matthias Naaf, M.Sc. LuFG Mathematische Grundlagen der Informatik

Thema: Logic, Semirings, and Fixed Points

Abstract:

Why does my SQL query return a particular answer? How does Hanna win an infinite graph game against Simon? These questions can be answered with semiring semantics, which was introduced by Green, Karvounarakis, and Tannen (2007) for database provenance and has since been extended to various logics within and beyond the database setting. In this talk, we study semiring semantics for the fixed-point logic LFP, which (despite its name) features both least and greatest fixed points.

The common theme in semiring semantics is the interplay of logic and algebra, such as the compatibility with semiring homomorphisms and the use of freely generated semirings to represent provenance information. This becomes particularly interesting for fixed-point logic, where additional algebraic and order-theoretic assumptions on the semirings must be made to ensure the existence of fixed points. A key question is the algorithmic computation of fixed points in these semirings. Several techniques have been developed for least fixed points, with the Newton iteration (Esparza, Kiefer, and Luttenberger, 2010) emerging as the most general technique, but it was not known how to compute greatest fixed points. We address this issue by providing an efficient closed-form solution for greatest fixed points of polynomial systems over absorptive semirings.

Using the example of Büchi games, we show how semiring semantics of LFP can be applied to analyse winning strategies in infinite games. Lastly, we take the perspective of model theory and study how the classical 0-1 laws about the asymptotic behaviour of logic on random structures can be generalised to semiring semantics of first-order logic. By combining our proof with the fixed-point computation, we further extend the 0-1 law to semiring semantics of LFP.

Es laden ein: die Dozentinnen und Dozenten der Informatik