Document Open Access Logo

Fluted Logic with Counting

Author Ian Pratt-Hartmann

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2021.141.pdf
  • Filesize: 0.75 MB
  • 17 pages

Document Identifiers

Author Details

Ian Pratt-Hartmann
  • Department of Computer Science, University of Manchester, UK
  • Institute of Computer Science, University of Opole, Poland

Funding

This work was supported by the Polish NCN, grant number 2018/31/B/ST6/03662.

Acknowledgements

The author wishes to thank Prof. L. Tendera for valuable discussions.

Cite As Get BibTex

Ian Pratt-Hartmann. Fluted Logic with Counting. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 141:1-141:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021) https://doi.org/10.4230/LIPIcs.ICALP.2021.141

Abstract

The fluted fragment is a fragment of first-order logic in which the order of quantification of variables coincides with the order in which those variables appear as arguments of predicates. It is known that the fluted fragment possesses the finite model property. In this paper, we extend the fluted fragment by the addition of counting quantifiers. We show that the resulting logic retains the finite model property, and that the satisfiability problem for its (m+1)-variable sub-fragment is in m-NExpTime for all positive m. We also consider the satisfiability and finite satisfiability problems for the extension of any of these fragments in which the fluting requirement applies only to sub-formulas having at least three free variables.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Fluted fragment
  • counting quantifiers
  • satisfiability
  • complexity

Metrics

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

References

  1. H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217-274, 1998. Google Scholar
  2. V. Báránay, B. ten Cate, and L. Segoufin. Guarded negation. Journal of the ACM, 62(3):22:1-26, 2015. Google Scholar
  3. M. Benedikt, E. Kostylev, and T. Tan. Two-variable logic with ultimately periodic counting. In A. Dawar A. Czumaj and E. Merelli, editors, Proc. of ICALP 2020, LIPIcs, pages 112:1-112:16. Schloß Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  4. I. Borosh and L. Treybig. Bounds on the positive integral solutions of linear Diophantine equations. Proceedings of the American Mathematical Society, 55(2):299-304, 1976. Google Scholar
  5. E. Grädel. On the restraining power of guards. Journal of Symbolic Logic, 64:1719-1742, 1999. Google Scholar
  6. E. Grädel, M. Otto, and E. Rosen. Two-variable logic with counting is decidable. In Logic in Computer Science, pages 306-317. IEEE, 1997. Google Scholar
  7. C. Haase. A survival guide to Presburger arithmetic. ACM SIGLOG News, 5(3):67-82, 2018. Google Scholar
  8. D. Hilbert and W. Ackermann. Grundzüge der mathematischen Logik. Springer, Berlin, 1st edition, 1928. Google Scholar
  9. D. Hilbert and W. Ackermann. Principles of Mathematical Logic. Chelsea, New York, 1950. Google Scholar
  10. E. Kieroński and S. Rudolph. Finite model theory of the triguarded fragment and related logics. To appear, Logic in Computer Science (LICS), 2021; arXiV preprint URL: https://arxiv.org/abs/2101.08377v2.
  11. L. Löwenheim. Über Möglichkeiten im Relativkalkül. Math. Annalen, 76:447-470, 1915. Google Scholar
  12. L. Pacholski, W. Szwast, and L. Tendera. Complexity results for two-variable first-order logic with counting. SIAM Journal of Computing, 29:1083-1117, 1999. Google Scholar
  13. C. Papadimitriou. On the complexity of integer programming. Journal of the ACM, 28(4):765-768, 1981. Google Scholar
  14. L. Pottier. Minimal solutions of linear Diophantine systems : bounds and algorithms. In R. Book, editor, Proc. Rewriting Techniques and Applications, volume 488 of LNCS, pages 162-173, Berlin, 1991. Springer. Google Scholar
  15. I. Pratt-Hartmann. Complexity of the two-variable fragment with counting quantifiers. Journal of Logic, Language and Information, 14(3):369-395, 2005. Google Scholar
  16. I. Pratt-Hartmann. The finite satisfiability problem for two-variable, first-order logic with one transitive relation is decidable. Mathematical Logic Quarterly, 64(3):218-248, 2018. Google Scholar
  17. I. Pratt-Hartmann, W. Szwast, and L. Tendera. The fluted fragment revisited. Journal of Symbolic Logic, 84(3):1020-1048, 2019. Google Scholar
  18. Ian Pratt-Hartmann and Lidia Tendera. The fluted fragment with transitive relations, 2020. URL: http://arxiv.org/abs/2006.11169.
  19. W. Purdy. Fluted formulas and the limits of decidability. Journal of Symbolic Logic, 61(2):608-620, 1996. Google Scholar
  20. W. Purdy. Complexity and nicety of fluted logic. Studia Logica, 71:177-198, 2002. Google Scholar
  21. W. V. Quine. Variables explained away. Proceedings of the American Philosophical Society, 104(3):343-347, 1960. Google Scholar
  22. W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62. University of Vienna, 1969. Google Scholar
  23. S. Rudolph and M. Šimkus. The triguarded fragment of first-order logic. In Proceedings of 22nd International Conference for Programming, Artificial Intelligence and Reasoning (LPAR-22), volume 57, pages 604-619. EPiC Series in Computing, 2018. Google Scholar
  24. S. Schmitz. Complexity hierarchies beyond Elementary. ACM Transactions on Computation Theory, 8(1:3):1-36, 2016. Google Scholar
  25. D. Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962. Google Scholar
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