Author name cluster

Matthias Naaf

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

CSL Conference 2026 Conference Paper

Compactness in Semiring Semantics

Sophie Brinke
Anuj Dawar
Erich Grädel
Lovro Mrkonjic
Matthias Naaf

Semiring provenance was originally introduced in database theory with the aim of explaining why certain tuples are (not) contained in the answer of a query. To this end, logical statements are not just evaluated to true or false but to values in a commutative semiring. Depending on the underlying semiring, this allows us to track descriptions of the atomic facts that are responsible for the truth of a statement or practical information about the evaluation such as costs or confidence. Recently, this approach has been expanded to a systematic study of semiring semantics for first-order logic and other logical systems. This raises the question to what extent model-theoretic results can be generalised to semiring semantics and how this relates to the algebraic properties of the underlying semiring. Here we investigate the availability of compactness in semiring semantics. The appropriate setting for this is based on absorptive semirings with well-defined infinitary products. Compactness can be stated either in terms of satisfiability or in terms of entailment, and these two variants are trivially equivalent in Boolean semantics. However, this is no longer the case in semiring semantics. Compactness in terms of satisfiability, defined as the existence of non-zero valuations, indeed generalises to every infinitary absorptive semiring. For compactness in terms of entailment the situation is different. The entailment relation naturally extends to semiring semantics (via the natural order on the semiring) but this yields a stronger variant of compactness, which fails for certain important semirings, including the tropical semiring and the Łukasiewicz semiring. Our main positive results show that strong compactness does indeed hold for all finite semirings and all lattice semirings.

Details

MFCS Conference 2023 Conference Paper

Locality Theorems in Semiring Semantics

Clotilde Bizière
Erich Grädel
Matthias Naaf

Semiring semantics of first-order logic generalises classical Boolean semantics by permitting truth values from a commutative semiring, which can model information such as costs or access restrictions. This raises the question to what extent classical model-theoretic properties still apply, and how this depends on the algebraic properties of the semiring. In this paper, we study this question for the classical locality theorems due to Hanf and Gaifman. We prove that Hanf’s locality theorem generalises to all semirings with idempotent operations, but fails for many non-idempotent semirings. We then consider Gaifman normal forms and show that for formulae with free variables, Gaifman’s theorem does not generalise beyond the Boolean semiring. Also for sentences, it fails in the natural semiring and the tropical semiring. Our main result, however, is a constructive proof of the existence of Gaifman normal forms for min-max and lattice semirings. The proof implies a stronger version of Gaifman’s classical theorem in Boolean semantics: every sentence has a Gaifman normal form which does not add negations.

Details

Highlights Conference 2023 Conference Abstract

Zero-One Laws in Semiring Semantics

Matthias Naaf

Semiring semantics evaluates logical statements by values in a commutative semiring, which can model information such as costs or access restrictions. Random semiring interpretations, induced by a probability distribution on the semiring, generalise random structures, which raises the question to what extent the classical 0-1 laws of first-order logic apply to semiring semantics. In this talk, we will see that a 0-1 law holds for for many semirings, that is, every first-order sentence asymptotically almost surely evaluates to a unique semiring value on random semiring interpretations. For finite and infinite lattice semirings, we further show that only three semiring values are possible: 0, 1, and the smallest non-zero value. The proof is a combination of the classical extension axioms and an algebraic representation of first-order sentences tailored to semiring semantics. Joint work with Erich Grädel, Hayyan Helal, and Richard Wilke. Contributed talk given by Matthias Naaf

Details

Highlights Conference 2021 Conference Abstract

Computing Least and Greatest Fixed Points in Absorptive Semirings

Matthias Naaf

This talk presents results on the computation of both least and greatest solutions of polynomial equation systems over absorptive semirings (with certain completeness and continuity assumptions) such as the tropical semiring, motivated by recent work on semiring provenance analysis of fixed-point logics. Our main result is a closed-form solution that needs only a polynomial number of semiring operations and an infinitary power operation. We prove this by considering (possibly infinite) derivation trees and showing that we only need trees of a certain shape: a reachability prefix with (infinite) deterministic subtrees. This talk is based on a paper submitted to RAMiCS 2021, a preprint is available at https: //arxiv. org/abs/2106. 00399.

Details

GandALF Workshop 2021 Workshop Paper

Semiring Provenance for Büchi Games: Strategy Analysis with Absorptive Polynomials

Erich Grädel
Niels Lücking
Matthias Naaf

This paper presents a case study for the application of semiring semantics for fixed-point formulae to the analysis of strategies in Büchi games. Semiring semantics generalizes the classical Boolean semantics by permitting multiple truth values from certain semirings. Evaluating the fixed-point formula that defines the winning region in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. This is well-understood for reachability games, where the winning region is definable as a least fixed point. The case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the fixed-point definition involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies - strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables applications such as game synthesis or determining minimal modifications to the game needed to change its outcome.

PDF Details DOI

CSL Conference 2021 Conference Paper

Semiring Provenance for Fixed-Point Logic

Katrin M. Dannert
Erich Grädel
Matthias Naaf
Val Tannen

Semiring provenance is a successful approach, originating in database theory, to providing detailed information on how atomic facts combine to yield the result of a query. In particular, general provenance semirings of polynomials or formal power series provide precise descriptions of the evaluation strategies or "proof trees" for the query. By evaluating these descriptions in specific application semirings, one can extract practical information for instance about the confidence of a query or the cost of its evaluation. This paper develops semiring provenance for very general logical languages featuring the full interaction between negation and fixed-point inductions or, equivalently, arbitrary interleavings of least and greatest fixed points. This also opens the door to provenance analysis applications for modal μ-calculus and temporal logics, as well as for finite and infinite model-checking games. Interestingly, the common approach based on Kleene’s Fixed-Point Theorem for ω-continuous semirings is not sufficient for these general languages. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, and (2) absorptive. Full continuity guarantees that provenance values of least and greatest fixed-points are well-defined. Absorptive semirings provide a symmetry between least and greatest fixed-points and make sure that provenance values of greatest fixed points are informative. We identify semirings of generalized absorptive polynomials S^{∞}[X] and prove universal properties that make them the most general appropriate semirings for our framework. These semirings have the further property of being (3) chain-positive, which is responsible for having truth-preserving interpretations that give non-zero values to all true formulae. We relate the provenance analysis of fixed-point formulae with provenance values of plays and strategies in the associated model-checking games. Specifically, we prove that the provenance value of a fixed point formula gives precise information on the evaluation strategies in these games.

Details