Researcher profile

Matthias Naaf

Matthias Naaf contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate

Trust snapshot

Quick read

Trust 13 - UnverifiedVerification L1Unclaimed author
2works
0followers
3topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

2 published item(s)

preprint2022arXiv

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

Semiring semantics evaluates logical statements by values in some commutative semiring K. Random semiring interpretations, induced by a probability distribution on K, generalise random structures, and we investigate here the question of how classical results on first-order logic on random structures, most importantly the 0-1 laws of Glebskii et al. and Fagin, generalise to semiring semantics. For positive semirings, the classical 0-1 law implies that every 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, we can prove much stronger results. For many semirings K, the first-order sentences can be partitioned into classes F(j) for all semiring values j in K, such that every sentence in F(j) evaluates almost surely to j under random semiring interpretations. Further, for finite or infinite lattice semirings, 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 smallest non-zero value e. The problem of computing the almost sure valuation of a first-order sentence on finite lattice semirings is PSPACE-complete. An important semiring where the analysis is somewhat different is the semiring of natural numbers. Here, both addition and multiplication are increasing with respect to the natural semiring order and the classes F(j), for natural numbers j, no longer cover all FO-sentences, but have to be extended by the class of sentences that almost surely evaluate to unboundedly large values.

preprint2020arXiv

Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic

Semiring provenance is a successful approach to provide detailed information on the combinations of atomic facts that are responsible for the result of a query. In particular, interpretations in general provenance semirings of polynomials or formal power series give precise descriptions of the successful evaluation strategies for the query. While provenance analysis in databases has, for a long time, been largely confined to negation-free query languages, a recent approach extends this to model checking problems for logics with full negation. Algebraically this relies on new quotient semirings of dual-indeterminate polynomials or power series. So far, this approach has been developed mainly for first-order logic and for the positive fragment of least fixed-point logic. What has remained open is an adequate treatment for fixed-point calculi that admit arbitrary interleavings of least and greatest fixed points. We show that an adequate framework for the provenance analysis of full fixed-point logics is provided by semirings that are (1) fully continuous, (2) absorptive, and (3) chain-positive. 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-point computations and make sure that provenance values of greatest fixed points are informative. Finally, chain-positivity is responsible for having truth-preserving interpretations, which give non-zero values to all true formulae. We further identify semirings of generalized absorptive polynomials and prove universal properties that make them the most general appropriate semirings for LFP. We illustrate the power of provenance interpretations in these semirings by relating them to provenance values of plays and strategies in the associated model-checking games.