Guest Talk: Lauri Hella: An NLOG fragment of inclusion logic
Monday, December 09, 2019, 4:00pm
Location: RWTH Aachen University, Department of Computer Science - Ahornstr. 55, building E1, Seminar room i7
Speaker: 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.