Document Open Access Logo

One-Dimensional Guarded Fragments

Author Emanuel Kieroński

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.16.pdf
  • Filesize: 0.49 MB
  • 14 pages

Document Identifiers

Author Details

Emanuel Kieroński
  • University of Wrocław, Poland

Funding

Supported by Polish National Science Centre grant No 2016/21/B/ST6/01444.

Acknowledgements

The author would like to thank Sebastian Rudolph and the anonymous reviewers for their helpful comments.

Cite As Get BibTex

Emanuel Kieroński. One-Dimensional Guarded Fragments. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 16:1-16:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.MFCS.2019.16

Abstract

We call a first-order formula one-dimensional if every maximal block of existential (or universal) quantifiers in it leaves at most one variable free. We consider the one-dimensional restrictions of the guarded fragment, GF, and the tri-guarded fragment, TGF, the latter being a recent extension of GF in which quantification for subformulas with at most two free variables need not be guarded, and which thus may be seen as a unification of GF and the two-variable fragment, FO^2. We denote the resulting formalisms, resp., GF_1, and TGF_1. We show that GF_1 has an exponential model property and NExpTime-complete satisfiability problem (that is, it is easier than full GF). For TGF_1 we show that it is decidable, has the finite model property, and its satisfiability problem is 2-ExpTime-complete (NExpTime-complete in the absence of equality). All the above-mentioned results are obtained for signatures with no constants. We finally discuss the impact of their addition, observing that constants do not spoil the decidability but increase the complexity of the satisfiability problem.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • guarded fragment
  • two-variable logic
  • satisfiability
  • finite model property

Metrics

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

Related Versions

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ány, G. Gottlob, and M. Otto. Querying the Guarded Fragment. Logical Methods in Computer Science, 10(2), 2014. Google Scholar
  3. V. Bárány, B. ten Cate, and L. Segoufin. Guarded Negation. J. ACM, 62(3):22, 2015. Google Scholar
  4. P. Bourhis, M. Morak, and A. Pieris. Making Cross Products and Guarded Ontology Languages Compatible. In International Joint Conference on Artificial Intelligence, IJCAI 2017, pages 880-886, 2017. Google Scholar
  5. A. K. Chandra, D. Kozen, and L. J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: https://doi.org/10.1145/322234.322243.
  6. W. D. Goldfarb. The unsolvability of the Gödel class with identity. J. Symb. Logic, 49:1237-1252, 1984. Google Scholar
  7. E. Grädel. On The Restraining Power of Guards. J. Symb. Log., 64(4):1719-1742, 1999. Google Scholar
  8. E. Grädel, P. Kolaitis, and M. Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53-69, 1997. Google Scholar
  9. L. Hella and A. Kuusisto. One-dimensional Fragment of First-order Logic. In Proceedings of Advances in Modal Logic, 2014, pages 274-293, 2014. Google Scholar
  10. A.S. Kahr, E.F. Moore, and H. Wang. Entscheidungsproblem reduced to the ∀ ∃ ∀ case. Proc. Nat. Acad. Sci. U.S.A., 48:365-377, 1962. Google Scholar
  11. Y. Kazakov. Saturation-based decision procedures for extensions of the guarded fragment. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, 2006. Google Scholar
  12. E. Kieroński. Results on the Guarded Fragment with Equivalence or Transitive Relations. In Computer Science Logic, volume 3634 of LNCS, pages 309-324. Springer, 2005. Google Scholar
  13. E. Kieronski and A. Kuusisto. Complexity and Expressivity of Uniform One-Dimensional Fragment with Equality. In MFCS. Proceedings, Part I, pages 365-376, 2014. Google Scholar
  14. M. Mortimer. On languages with two variables. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21:135-140, 1975. Google Scholar
  15. Sebastian Rudolph and Mantas Šimkus. The Triguarded Fragment of First-Order Logic. In LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 57 of EPiC Series in Computing, pages 604-619, 2018. Google Scholar
  16. B. ten Cate and L. Segoufin. Unary negation. Logical Methods in Comp. Sc., 9(3), 2013. Google Scholar
  17. J. van Benthem. Dynamic bits and pieces. ILLC Research Report, 1997. 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