Author name cluster

Lucas Heimberg

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.

3 papers

1 author row

Highlights Conference 2016 Conference Abstract

Hanf normal form for first-order logic with unary counting quantifiers

Lucas Heimberg
Dietrich Kuske
Nicole Schweikardt

This talk is based on the paper “Hanf normal form for first-order logic with unary counting quantifiers” co-authored by Lucas Heimberg (Humboldt-Universität zu Berlin), Dietrich Kuske (Technische Universität Ilmenau), and Nicole Schweikardt (Humboldt-Universität zu Berlin), which got accepted for LICS 2016. The paper can be downloaded under http: //www2. informatik. hu-berlin. de/logik/research/HKS-LICS16. pdf. We study the existence of Hanf normal forms for extensions FO(Qs) of first-order logic by sets Qs of unary counting quantifiers, i. e. , sets of subsets of the natural numbers. A formula is in Hanf normal form if it is a Boolean combination of formulas zeta describing the isomorphism type of a local neighbourhood around its free variables and statements of the form “the number of witnesses y of psi(y) belongs to (Q+k)” where Q in Qs, k is a natural number, and psi describes the isomorphism type of a local neighbourhood around its unique free variable y. We show that a formula from FO(Qs) can be transformed into a formula in Hanf normal form that is equivalent on all structures of degree at most d if, and only if, all counting quantifiers occurring in the formula are ultimately periodic. This transformation can be carried out in worst-case optimal 3-fold exponential time. In particular, this yields an algorithmic version of Nurmonen’s extension of Hanf’s theorem for first-order logic with modulo-counting quantifiers. As an immediate consequence, we obtain that on finite structures of degree at most d, model checking of first-order logic with modulo-counting quantifiers is fixed-parameter tractable.

Details

Highlights Conference 2014 Conference Abstract

Preservation and Decomposition Theorems for Bounded Degree Structures

Lucas Heimberg

This talk is based on the CSL-LICS '14 paper Preservation and decomposition theorems for bounded degree structures co-authored by Frederik Harwath, Lucas Heimberg, and Nicole Schweikardt (Goethe-University Frankfurt am Main) [link]. In this paper, we provide elementary algorithms for two preservation theorems for first-order sentences with modulo m counting quantifiers (FO+mod m ) on the class C d of all finite structures of degree at most d: For each FO+mod m -sentence that is preserved under extensions (homomorphisms) on C d, a C d -equivalent existential (existential-positive) FO-sentence can be constructed in 6-fold (4-fold) exponential time. For FO-sentences, the algorithm has 5-fold (4-fold) exponential time complexity. This is complemented by lower bounds showing that for FO-sentences a 3-fold exponential blow-up of the computed existential (existential-positive) sentence is unavoidable. In this talk, I will focus on a third contribution of our paper, concerning Feferman-Vaught decompositions. The classical Feferman-Vaught theorem states that for certain forms of compositions of structures (like disjoint unions and cartesian products), the theory of a structure composed from simpler structures is determined by the theories of the simpler structures. Algorithmic versions of such decomposition theorems are typically of the following form: A given FO-sentence that shall be evaluated in a composition of structures can be transformed into a decomposition, that is, a Boolean combination of FO-sentences that each are evaluated in only one component structure. It is known that even when restricted to disjoint unions of tree structures, a non-elementary complexity for such an algorithmen is unavoidable (Dawar, Grohe, Kreutzer, Schweikardt 2007). Here, we restrict our attention to the classes C d for d ≥ 2. We provide an algorithm that computes decompositions, that are equivalent to the input FO-formula on disjoint unions of a finite number of structures from C d for d ≥ 3 ( d ≥ 2). The algorithm’s running time is 3-fold (2-fold) exponential in the size of the input formula. This is achieved by employing an elementary construction for Hanf normal forms (Bollig, Kuske 2012) and decomposing the resulting Hanf-formulas. Our algorithm is optimal in the following sense: Even on binary forests (unions of labeled chains), that is, classes of structures of degree at most 3 (respectively, 2), a 3-fold (2-fold) exponential blow-up of the size of decompositions in terms of the size of the input formula is unavoidable. 11: 45 12: 00 Break

PDF Details

Highlights Conference 2013 Conference Abstract

An optimal Gaifman normal form construction for structures of bounded degree

Lucas Heimberg
Dietrich Kuske
Nicole Schweikardt

This paper's main result presents a $3$-fold exponential algorithm that transforms a first-order formula $\varphi$ together with a number $d$ into a formula in Gaifman normal form that is equivalent to $\varphi$ on the class of structures of degree at most~$d$. For structures of polynomial growth, we even get a $2$-fold exponential algorithm. These results are complemented by matching lower bounds: We show that for structures of degree $2$, a $2$-fold exponential blow-up in the size of formulas cannot be avoided. And for structures of degree $3$, a $3$-fold exponential blow-up is unavoidable. As a result of independent interest we obtain a $1$-fold exponential algorithm which transforms a given first-order sentence~$\varphi$ of a very restricted shape into a sentence in Gaifman normal form that is equivalent to $\varphi$ on all structures.

PDF Details