Document Open Access Logo

Finite Satisfiability of Unary Negation Fragment with Transitivity

Authors Daniel Danielski, Emanuel Kieroński

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2019.17.pdf
  • Filesize: 0.51 MB
  • 15 pages

Document Identifiers

Author Details

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

Funding

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

Cite AsGet BibTex

Daniel Danielski and Emanuel Kieroński. Finite Satisfiability of Unary Negation Fragment with Transitivity. In 44th International Symposium on Mathematical Foundations of Computer Science (MFCS 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 138, pp. 17:1-17:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.MFCS.2019.17

Abstract

We show that the finite satisfiability problem for the unary negation fragment with an arbitrary number of transitive relations is decidable and 2-ExpTime-complete. Our result actually holds for a more general setting in which one can require that some binary symbols are interpreted as arbitrary transitive relations, some as partial orders and some as equivalences. We also consider finite satisfiability of various extensions of our primary logic, in particular capturing the concepts of nominals and role hierarchies known from description logic. As the unary negation fragment can express unions of conjunctive queries, our results have interesting implications for the problem of finite query answering, both in the classical scenario and in the description logics setting.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • unary negation fragment
  • transitivity
  • finite satisfiability
  • finite open-world query answering
  • description logics

Metrics

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

Related Versions

References

  1. A. Amarilli, M. Benedikt, P. Bourhis, and M. Vanden Boom. Query Answering with Transitive and Linear-Ordered Data. In Proceedings of the 25th International Joint Conference on Artificial Intelligence, IJCAI 2016, pages 893-899, 2016. Google Scholar
  2. 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
  3. J.-F. Baget, M. LeClere, and M.-L. Mugnier. Walking the Decidability Line for Rules with Existential Variables. In Proceedings of the 12th International Conference on Principles of Knowledge Representation and Reasoning, KR 2010, pages 466-476, 2010. Google Scholar
  4. J.-F. Baget, M. Leclère, M.-L. Mugnier, and E. Salvat. Extending Decidable Cases for Rules with Existential Variables. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009, pages 677-682, 2009. Google Scholar
  5. V. Bárány, B. ten Cate, and L. Segoufin. Guarded Negation. J. ACM, 62(3):22, 2015. Google Scholar
  6. A. Calì, G. Gottlob, and M. Kifer. Taming the Infinite Chase: Query Answering under Expressive Relational Constraints. J. Artif. Intell. Res., 48:115-174, 2013. Google Scholar
  7. D. Danielski and E. Kieroński. Unary negation fragment with equivalence relations has the finite model property. In 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, pages 285-294, 2018. Google Scholar
  8. D. Danielski and E. Kieronski. Unary negation fragment with equivalence relations has the finite model property. CoRR, abs/1802.01318, 2018. URL: http://arxiv.org/abs/1802.01318.
  9. M. Dzieciołowski. Satisfability issues for unary negation logic. Bachelor’s thesis, University of Wrocław, 2017. Google Scholar
  10. H. Ganzinger, Ch. Meyer, and M. Veanes. The Two-Variable Guarded Fragment with Transitive Relations. In 14th Annual IEEE Symposium on Logic in Computer Science, LICS 1999, pages 24-34, 1999. Google Scholar
  11. B. Glimm and Y. Kazakov. Role Conjunctions in Expressive Description Logics. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, pages 391-405, 2008. Google Scholar
  12. T. Gogacz, Y. A. Ibáñez-García, and F. Murlak. Finite Query Answering in Expressive Description Logics with Transitive Roles. In Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018., pages 369-378, 2018. Google Scholar
  13. E. Grädel. On The Restraining Power of Guards. J. Symb. Log., 64(4):1719-1742, 1999. Google Scholar
  14. 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
  15. E. Grädel, M. Otto, and E. Rosen. Undecidability results on two-variable logics. Archiv für Mathematische Logik und Grundlagenforschung, 38(4-5):313-354, 1999. Google Scholar
  16. J. Ch. Jung, C. Lutz, M. Martel, and T. Schneider. Querying the Unary Negation Fragment with Regular Path Expressions. In International Conference on Database Theory, ICDT 2018, pages 15:1-15:18, 2018. Google Scholar
  17. Y. Kazakov. Saturation-based decision procedures for extensions of the guarded fragment. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, 2006. Google Scholar
  18. 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
  19. E. Kieroński. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006. Google Scholar
  20. E. Kieroński and L. Tendera. Finite Satisfiability of the Two-Variable Guarded Fragment with Transitive Guards and Related Variants. ACM Trans. Comput. Logic, 19(2):8:1-8:34, 2018. Google Scholar
  21. I. Pratt-Hartmann. The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable. Mathematical Logic Quarterly, 2018. Google Scholar
  22. I. Pratt-Hartmann, W. Szwast, and L. Tendera. The Fluted Fragment Revisited. Journal of Symbolic Logic, Forthcoming, 2019. Google Scholar
  23. I. Pratt-Hartmann and L. Tendera. The Fluted Fragment with Transitivity. In 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, pages 18:1-18:15, 2019. Google Scholar
  24. W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62, 1969. Google Scholar
  25. D. Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962. Google Scholar
  26. W. Szwast and L. Tendera. The guarded fragment with transitive guards. Annals of Pure and Applied Logic, 128:227-276, 2004. Google Scholar
  27. B. ten Cate and L. Segoufin. Unary negation. Logical Methods in Comp. Sc., 9(3), 2013. 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 Imprint Privacy Contact