Skip to Main content Skip to Navigation
Journal articles

An optimal construction of Hanf sentences

Benedikt Bollig 1, 2 Dietrich Kuske 3
1 LSV - Laboratoire Spécification et Vérification [Cachan]
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], Inria Saclay - Ile de France
3 TU - Technische Universität Ilmenau
Abstract : We give a new construction of formulas in Hanf normal form that are equivalent to first-order formulas over structures of bounded degree. This is the first algorithm whose running time is shown to be elementary. The triply exponential upper bound is complemented by a matching lower bound.
Document type :
Journal articles
Complete list of metadata
https://hal.inria.fr/hal-00776607
Contributor : Benedikt Bollig <>
Submitted on : Tuesday, January 15, 2013 - 5:48:17 PM
Last modification on : Friday, April 2, 2021 - 8:38:05 AM

Links full text

openaccess

Identifiers

Collections

CNRS | INRIA | ENS-CACHAN | INSMI | ENS-PARIS-SACLAY

Citation

Benedikt Bollig, Dietrich Kuske. An optimal construction of Hanf sentences. Journal of Applied Logic, Elsevier, 2012, 10 (2), pp.179-186. ⟨10.1016/j.jal.2012.01.002⟩. ⟨hal-00776607⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

288

 

Contact                    Legal Notice                    Personal Data