Document Open Access Logo

Gaifman Normal Forms for Counting Extensions of First-Order Logic

Authors Dietrich Kuske, Nicole Schweikardt

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2018.133.pdf
  • Filesize: 0.5 MB
  • 14 pages

Document Identifiers

Author Details

Dietrich Kuske
  • Technische Universität Ilmenau, Germany
Nicole Schweikardt
  • Humboldt-Universität zu Berlin, Germany

Funding

  • Schweikardt, Nicole: Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) - SCHW 837/5-1.

Cite As Get BibTex

Dietrich Kuske and Nicole Schweikardt. Gaifman Normal Forms for Counting Extensions of First-Order Logic. In 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 107, pp. 133:1-133:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.ICALP.2018.133

Abstract

We consider the extension of first-order logic FO by unary counting quantifiers and generalise the notion of Gaifman normal form from FO to this setting. For formulas that use only ultimately periodic counting quantifiers, we provide an algorithm that computes equivalent formulas in Gaifman normal form. We also show that this is not possible for formulas using at least one quantifier that is not ultimately periodic.
Now let d be a degree bound. We show that for any formula phi with arbitrary counting quantifiers, there is a formula gamma in Gaifman normal form that is equivalent to phi on all finite structures of degree <= d. If the quantifiers of phi are decidable (decidable in elementary time, ultimately periodic), gamma can be constructed effectively (in elementary time, in worst-case optimal 3-fold exponential time).
For the setting with unrestricted degree we show that by using our Gaifman normal form for formulas with only ultimately periodic counting quantifiers, a known fixed-parameter tractability result for FO on classes of structures of bounded local tree-width can be lifted to the extension of FO with ultimately periodic counting quantifiers (a logic equally expressive as FO+MOD, i.e., first-oder logic with modulo-counting quantifiers).

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Finite model theory
  • Gaifman locality
  • modulo-counting quantifiers
  • fixed parameter tractable model-checking

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. S. Arnborg, J. Lagergren, and D. Seese. Easy problems for tree-decomposable graphs. J. Algorithms, 12(2):308-340, 1991. URL: http://dx.doi.org/10.1016/0196-6774(91)90006-K.
  2. B. Bollig and D. Kuske. An optimal construction of Hanf sentences. J. Applied Logic, 10(2):179-186, 2012. URL: http://dx.doi.org/10.1016/j.jal.2012.01.002.
  3. B. Courcelle. The monadic second-order logic of graphs. I. Recognizable sets of finite graphs. Inf. Comput., 85(1):12-75, 1990. URL: http://dx.doi.org/10.1016/0890-5401(90)90043-H.
  4. A. Dawar, M. Grohe, S. Kreutzer, and N. Schweikardt. Model theory makes formulas large. In Proceedings of the 34th International Colloquium on Automata, Languages and Programming, ICALP 2007, Wroclaw, Poland, July 9-13, 2007, pages 913-924, 2007. URL: http://dx.doi.org/10.1007/978-3-540-73420-8_78.
  5. J. Doner. Tree acceptors and some of their applications. J. Comput. Syst. Sci., 4(5):406-451, 1970. URL: http://dx.doi.org/10.1016/S0022-0000(70)80041-1.
  6. Z. Dvorak, D. Král, and R. Thomas. Deciding first-order properties for sparse graphs. In Proceedings of the 51st Annual IEEE Symposium on Foundations of Computer Science, FOCS 2010, October 23-26, 2010, Las Vegas, Nevada, USA, pages 133-142, 2010. URL: http://dx.doi.org/10.1109/FOCS.2010.20.
  7. H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Perspectives in Mathematical Logic. Springer, 1995. Google Scholar
  8. S. Feferman and R. L. Vaught. The first-order properties of products of algebraic systems. Fundamenta Mathematicae, 47:57-103, 1959. Google Scholar
  9. M. Frick and M. Grohe. Deciding first-order properties of locally tree-decomposable structures. J. ACM, 48(6):1184-1206, 2001. URL: http://dx.doi.org/10.1145/504794.504798.
  10. H. Gaifman. On local and nonlocal properties. In J. Stern, editor, Logic Colloquium '81, pages 105-135. North-Holland, 1982. Google Scholar
  11. M. Grohe. Logic, graphs, and algorithms. In Logic and Automata: History and Perspectives [in Honor of Wolfgang Thomas], volume 2 of Texts in Logic and Games, pages 357-422. Amsterdam University Press, 2008. Google Scholar
  12. M. Grohe, S. Kreutzer, and S. Siebertz. Deciding first-order properties of nowhere dense graphs. J. ACM, 64(3):17:1-17:32, 2017. URL: http://dx.doi.org/10.1145/3051095.
  13. F. Harwath, L. Heimberg, and N. Schweikardt. Preservation and decomposition theorems for bounded degree structures. Logical Methods in Computer Science, 11(4), 2015. URL: http://dx.doi.org/10.2168/LMCS-11(4:17)2015.
  14. F. Harwath and N. Schweikardt. On the locality of arb-invariant first-order formulas with modulo counting quantifiers. Logical Methods in Computer Science, 12(4), 2016. URL: http://dx.doi.org/10.2168/LMCS-12(4:8)2016.
  15. L. Heimberg. Complexity of normal forms on structures of bounded degree. PhD thesis, Humboldt-Universität zu Berlin, 2017. Google Scholar
  16. L. Heimberg, D. Kuske, and N. Schweikardt. An optimal Gaifman normal form construction for structures of bounded degree. In Proceedings of the 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013, pages 63-72, 2013. URL: http://dx.doi.org/10.1109/LICS.2013.11.
  17. L. Heimberg, D. Kuske, and N. Schweikardt. Hanf normal form for first-order logic with unary counting quantifiers. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, New York, NY, USA, July 5-8, 2016, pages 277-286, 2016. URL: http://dx.doi.org/10.1145/2933575.2934571.
  18. L. Hella, L. Libkin, and J. Nurmonen. Notions of locality and their logical characterizations over finite models. J. Symb. Log., 64(4):1751-1773, 1999. URL: http://dx.doi.org/10.2307/2586810.
  19. D. Kuske and N. Schweikardt. First-order logic with counting. In Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1-12, 2017. (Full version available at https://arxiv.org/abs/1703.01122). URL: http://dx.doi.org/10.1109/LICS.2017.8005133.
  20. L. Libkin. Elements of Finite Model Theory. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. URL: http://dx.doi.org/10.1007/978-3-662-07003-1.
  21. J. A. Makowsky. Algorithmic uses of the Feferman-Vaught Theorem. Ann. Pure Appl. Logic, 126(1-3):159-213, 2004. URL: http://dx.doi.org/10.1016/j.apal.2003.11.002.
  22. A. B. Matos. Periodic sets of integers. Theor. Comput. Sci., 127(2):287-312, 1994. URL: http://dx.doi.org/10.1016/0304-3975(94)90044-2.
  23. H. Niemistö. Locality and Order-Invariant Logics. PhD thesis, Department of Mathematics and Statistics, University of Helsinki, 2007. Google Scholar
  24. J. Nurmonen. Counting modulo quantifiers on finite structures. Inf. Comput., 160(1-2):62-87, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2842.
  25. D. Seese. Linear time computable problems and first-order descriptions. Mathematical Structures in Computer Science, 6(6):505-526, 1996. Google Scholar
  26. H. Straubing. Finite automata, formal logic, and circuit complexity. Progress in Theoretical Computer Science. Birkhäuser Boston Inc., Boston, MA, 1994. Google Scholar
  27. J. W. Thatcher and J. B. Wright. Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory, 2(1):57-81, 1968. URL: http://dx.doi.org/10.1007/BF01691346.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact