An optimal construction of Hanf sentences

Benedikt Bollig 1, 2 Dietrich Kuske 3
2 MEXICO - Modeling and Exploitation of Interaction and Concurrency
LSV - Laboratoire Spécification et Vérification [Cachan], ENS Cachan - École normale supérieure - Cachan, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8643
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.
Type de document :
Article dans une revue
Journal of Applied Logic, Elsevier, 2012, 10 (2), pp.179-186. 〈10.1016/j.jal.2012.01.002〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00776607
Contributeur : Benedikt Bollig <>
Soumis le : mardi 15 janvier 2013 - 17:48:17
Dernière modification le : jeudi 11 janvier 2018 - 06:23:37

Lien texte intégral

Identifiants

Collections

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〉

Partager

Métriques

Consultations de la notice

202