Gastvortrag: Lauri Hella: An NLOG fragment of inclusion logic
Montag, 09.12.2019, 16.00 Uhr
Ort: RWTH Aachen University, Informatikzentrum - Ahornstr. 55, Erweiterungsgebäude E1, Seminar room i7
Vortragender: Lauri Hella (Tampere)
Inclusion logic is known to have the same expressive power as greatest fixed-point logic. Thus, by the Immerman-Vardi Theorem, it captures PTIME on the class O of finite ordered
structures. We introduce a syntactic fragment on inclusion logic that captures NLOG on O.
In order to analyze the complexity of the model-checking problem MC(phi) of inclusion logic
formulas, we study the closely related maximal subteam membership problem MSM(phi):
given a structure A, a team X and and assignment s, does s belong to the largest subteam of X
that satisfies phi in A? We show that if MSM(phi) is in NLOG, then so is MC(phi). Furthermore,
we show that MSM(phi) is in NLOG for any inclusion atom, and certain natural operators
preserve the complexity of MSM. Finally we show that the fragment obtained by closing
inclusion atoms and first-order literals by these operators can simulate transitive closure logic
on the class O.