Finite Satisfiability of Unary Negation Fragment with Transitivity
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.
unary negation fragment
transitivity
finite satisfiability
finite open-world query answering
description logics
Theory of computation~Logic
17:1-17:15
Regular Paper
Supported by Polish National Science Centre grant No 2016/21/B/ST6/01444.
A full version of this paper is available at https://arxiv.org/abs/1809.03245.
Daniel
Danielski
Daniel Danielski
University of Wrocław, Poland
Emanuel
Kieroński
Emanuel Kieroński
University of Wrocław, Poland
https://orcid.org/0000-0002-8538-8221
10.4230/LIPIcs.MFCS.2019.17
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.
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.
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.
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.
V. Bárány, B. ten Cate, and L. Segoufin. Guarded Negation. J. ACM, 62(3):22, 2015.
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.
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.
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.
http://arxiv.org/abs/1802.01318
M. Dzieciołowski. Satisfability issues for unary negation logic. Bachelor’s thesis, University of Wrocław, 2017.
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.
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.
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.
E. Grädel. On The Restraining Power of Guards. J. Symb. Log., 64(4):1719-1742, 1999.
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.
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.
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.
Y. Kazakov. Saturation-based decision procedures for extensions of the guarded fragment. PhD thesis, Universität des Saarlandes, Saarbrücken, Germany, 2006.
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.
E. Kieroński. On the complexity of the two-variable guarded fragment with transitive guards. Inf. Comput., 204(11):1663-1703, 2006.
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.
I. Pratt-Hartmann. The Finite Satisfiability Problem for Two-Variable, First-Order Logic with one Transitive Relation is Decidable. Mathematical Logic Quarterly, 2018.
I. Pratt-Hartmann, W. Szwast, and L. Tendera. The Fluted Fragment Revisited. Journal of Symbolic Logic, Forthcoming, 2019.
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.
W. V. Quine. On the limits of decision. In Proceedings of the 14th International Congress of Philosophy, volume III, pages 57-62, 1969.
D. Scott. A decision method for validity of sentences in two variables. Journal Symbolic Logic, 27:477, 1962.
W. Szwast and L. Tendera. The guarded fragment with transitive guards. Annals of Pure and Applied Logic, 128:227-276, 2004.
B. ten Cate and L. Segoufin. Unary negation. Logical Methods in Comp. Sc., 9(3), 2013.
Daniel Danielski and Emanuel Kieroński
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode