Document Open Access Logo

On the Complexity of Team Logic and Its Two-Variable Fragment

Author Martin Lück

PDF
Thumbnail PDF

File

LIPIcs.MFCS.2018.27.pdf
  • Filesize: 0.61 MB
  • 22 pages

Document Identifiers

Author Details

Martin Lück
  • Institut für Theoretische Informatik, Leibniz Universität Hannover, Appelstraße 4, 30167 Hannover, Germany

Cite AsGet BibTex

Martin Lück. On the Complexity of Team Logic and Its Two-Variable Fragment. In 43rd International Symposium on Mathematical Foundations of Computer Science (MFCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 117, pp. 27:1-27:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.MFCS.2018.27

Abstract

We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown to be axiomatizable, but otherwise has not yet received much attention in questions of computational complexity. In this paper, we consider its two-variable fragment FO^2(~) and prove that its satisfiability problem is decidable, and in fact complete for the recently introduced non-elementary class TOWER(poly). Moreover, we classify the complexity of model checking of FO(~) with respect to the number of variables and the quantifier rank, and prove a dichotomy between PSPACE- and ATIME-ALT(exp, poly)-complete fragments. For the lower bounds, we propose a translation from modal team logic MTL to FO^2(~) that extends the well-known standard translation from modal logic ML to FO^2. For the upper bounds, we translate FO(~) to fragments of second-order logic with PSPACE-complete and ATIME-ALT(exp, poly)-complete model checking, respectively.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
  • Theory of computation → Logic
Keywords
  • team logic
  • two-variable logic
  • complexity
  • satisfiability
  • model checking

Metrics

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

Related Versions

References

  1. Samson Abramsky, Juha Kontinen, Jouko Väänänen, and Heribert Vollmer, editors. Dependence Logic, Theory and Applications. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-31803-5.
  2. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philosophical Logic, 27(3):217-274, 1998. URL: http://dx.doi.org/10.1023/A:1004275029985.
  3. Vince Bárány and Mikołaj Bojańczyk. Finite satisfiability for guarded fixpoint logic. Inf. Process. Lett., 112(10):371-375, 2012. URL: http://dx.doi.org/10.1016/j.ipl.2012.02.005.
  4. Leonard Berman. The complexitiy of logical theories. Theor. Comput. Sci., 11:71-77, 1980. URL: http://dx.doi.org/10.1016/0304-3975(80)90037-7.
  5. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal logic. Cambridge University Press, New York, NY, USA, 2001. Google Scholar
  6. Egon Börger, Erich Grädel, and Yuri Gurevich. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, 1997. Google Scholar
  7. Ashok K. Chandra, Dexter C. Kozen, and Larry J. Stockmeyer. Alternation. J. ACM, 28(1):114-133, 1981. URL: http://dx.doi.org/10.1145/322234.322243.
  8. Arnaud Durand, Juha Kontinen, and Heribert Vollmer. Expressivity and Complexity of Dependence Logic. In Samson Abramsky, Juha Kontinen, Jouko Väänänen, and Heribert Vollmer, editors, Dependence Logic, pages 5-32. Springer International Publishing, 2016. URL: http://dx.doi.org/10.1007/978-3-319-31803-5_2.
  9. Johannes Ebbing, Lauri Hella, Arne Meier, Julian-Steffen Müller, Jonni Virtema, and Heribert Vollmer. Extended modal dependence logic. In Logic, Language, Information, and Computation - 20th International Workshop, WoLLIC 2013., pages 126-137, 2013. URL: http://dx.doi.org/10.1007/978-3-642-39992-3_13.
  10. Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Logic, 163(1):68-84, 2012. URL: http://dx.doi.org/10.1016/j.apal.2011.08.005.
  11. Pietro Galliani. General Models and Entailment Semantics for Independence Logic. Notre Dame Journal of Formal Logic, 54(2):253-275, 2013. URL: http://dx.doi.org/10.1215/00294527-1960506.
  12. Pietro Galliani. Upwards closed dependencies in team semantics. Inf. Comput., 245:124-135, 2015. URL: http://dx.doi.org/10.1016/j.ic.2015.06.008.
  13. Pietro Galliani. On strongly first-order dependencies. In Dependence Logic, Theory and Applications, pages 53-71. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-319-31803-5_4.
  14. Erich Grädel. Model-checking games for logics of imperfect information. Theor. Comput. Sci., 493:2-14, 2013. URL: http://dx.doi.org/10.1016/j.tcs.2012.10.033.
  15. Erich Grädel, Phokion G. Kolaitis, Leonid Libkin, Maarten Marx, Joel Spencer, Moshe Y. Vardi, Yde Venema, and Scott Weinstein. Finite Model Theory and Its Applications. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2007. URL: http://dx.doi.org/10.1007/3-540-68804-8.
  16. Erich Grädel, Martin Otto, and Eric Rosen. Two-variable logic with counting is decidable. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, 1997, pages 306-317, 1997. URL: http://dx.doi.org/10.1109/LICS.1997.614957.
  17. Erich Grädel and Jouko Väänänen. Dependence and independence. Studia Logica, 101(2):399-410, 2013. URL: http://dx.doi.org/10.1007/s11225-013-9479-2.
  18. Erich Grädel and Igor Walukiewicz. Guarded fixed point logic. In 14th Annual IEEE Symposium on Logic in Computer Science, pages 45-54, 1999. URL: http://dx.doi.org/10.1109/LICS.1999.782585.
  19. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. Bulletin of Symbolic Logic, 3(1):53–69, 1997. URL: http://dx.doi.org/10.2307/421196.
  20. Miika Hannula, Juha Kontinen, Martin Lück, and Jonni Virtema. On quantified propositional logics and the exponential time hierarchy. In Proceedings of the Seventh International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2016., pages 198-212, 2016. URL: http://dx.doi.org/10.4204/EPTCS.226.14.
  21. Miika Hannula, Juha Kontinen, Jonni Virtema, and Heribert Vollmer. Complexity of Propositional Logics in Team Semantic. ACM Transactions on Computational Logic, 19(1):1-14, jan 2018. URL: http://dx.doi.org/10.1145/3157054.
  22. Wilfrid Hodges. Compositional semantics for a language of imperfect information. Logic Journal of IGPL, 5(4):539-563, 1997. URL: http://dx.doi.org/10.1093/jigpal/5.4.539.
  23. Juha Kontinen, Antti Kuusisto, Peter Lohmann, and Jonni Virtema. Complexity of two-variable dependence logic and IF-logic. Information and Computation, 239:237-253, 2014. URL: http://dx.doi.org/10.1016/j.ic.2014.08.004.
  24. Juha Kontinen, Antti Kuusisto, and Jonni Virtema. Decidability of Predicate Logics with Team Semantics. In 41st International Symposium on Mathematical Foundations of Computer Science (MFCS 2016), volume 58 of Leibniz International Proceedings in Informatics (LIPIcs), pages 60:1-60:14, 2016. URL: http://dx.doi.org/10.4230/LIPIcs.MFCS.2016.60.
  25. Juha Kontinen and Ville Nurmi. Team logic and second-order logic. Fundam. Inform., 106(2-4):259-272, 2011. URL: http://dx.doi.org/10.3233/FI-2011-386.
  26. Antti Kuusisto. A Double Team Semantics for Generalized Quantifiers. Journal of Logic, Language and Information, 24(2):149-191, 2015. URL: http://dx.doi.org/10.1007/s10849-015-9217-4.
  27. Leopold Löwenheim. Über möglichkeiten im relativkalkül. Mathematische Annalen, 76:447-470, 1915. URL: http://eudml.org/doc/158703.
  28. Martin Lück. Canonical Models and the Complexity of Modal Team Logic. Computer Science Logic (CSL) 2018. To appear. Google Scholar
  29. Martin Lück. Axiomatizations of team logics. Annals of Pure and Applied Logic, 169(9):928-969, 2018. URL: http://dx.doi.org/10.1016/j.apal.2018.04.010.
  30. Martin Lück. On the Complexity of Team Logic and its Two-Variable Fragment. CoRR, abs/1804.04968, 2018. URL: https://arxiv.org/abs/1804.04968.
  31. Michael Mortimer. On languages with two variables. Math. Log. Q., 21(1):135-140, 1975. URL: http://dx.doi.org/10.1002/malq.19750210118.
  32. Julian-Steffen Müller. Satisfiability and model checking in team based logics. PhD thesis, University of Hanover, 2014. URL: http://d-nb.info/1054741921.
  33. Ian Pratt-Hartmann. The two-variable fragment with counting revisited. In Logic, Language, Information and Computation, 17th International Workshop, WoLLIC 2010., pages 42-54, 2010. URL: http://dx.doi.org/10.1007/978-3-642-13824-9_4.
  34. Frank P. Ramsey. On a Problem of Formal Logic, pages 1-24. Birkhäuser Boston, Boston, MA, 1987. URL: http://dx.doi.org/10.1007/978-0-8176-4842-8_1.
  35. Dana Scott. A decision method for validity of sentences in two variables. Journal of Symbolic Logic, 27(4):477, 1962. Google Scholar
  36. Thomas Sturm, Marco Voigt, and Christoph Weidenbach. Deciding first-order satisfiability when universal and existential variables are separated. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, pages 86-95, 2016. URL: http://dx.doi.org/10.1145/2933575.2934532.
  37. Marco Voigt. A fine-grained hierarchy of hard problems in the separated fragment. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, pages 1-12, 2017. URL: http://dx.doi.org/10.1109/LICS.2017.8005094.
  38. Jouko Väänänen. Dependence logic: A New Approach to Independence Friendly Logic. Number 70 in London Mathematical Society student texts. Cambridge University Press, Cambridge ; New York, 2007. Google Scholar
  39. Fan Yang. On extensions and variants of dependence logic. PhD thesis, University of Helsinki, 2014. URL: http://www.math.helsinki.fi/logic/people/fan.yang/dissertation_fyang.pdf.
  40. Fan Yang and Jouko Väänänen. Propositional team logics. Ann. Pure Appl. Logic, 168(7):1406-1441, 2017. URL: http://dx.doi.org/10.1016/j.apal.2017.01.007.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact