Guarded Hybrid Team Logics

Author Marius Tritschler

Thumbnail PDF


  • Filesize: 0.82 MB
  • 22 pages

Document Identifiers

Author Details

Marius Tritschler
  • Technische Universität Darmstadt, Germany

Cite AsGet BibTex

Marius Tritschler. Guarded Hybrid Team Logics. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 48:1-48:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Team logics are extensions of first-order logic where formulae are not evaluated over assignments, but over sets ("teams") of assignments. In its most basic form, this does not increase the expressiveness of the logic because we can only form statements about the common properties of all assignments ("flatness"). Therefore, additional "team atoms" are introduced to allow for assertions about interdependencies between the assignments like dependence or inclusion. We propose to consider binders known from hybrid logic to increase the expressiveness, where the bound teams may then be referenced as regular relations. We call this hybrid team logic (HTL). Additionally, we define the positive and negative fragments of HTL (HTL^+ and HTL^-) by requiring that relations that arise from binding only occur positively or negatively, respectively. We find that HTL and its positive and negative fragments are equivalent to prominent team logics: HTL^+ is eqivalent to inclusion logic, HTL^- is equivalent to exclusion/dependence logic and HTL itself is equivalent to independence or inclusion/exclusion logic. This classifies HTL as equivalent to existential second order logic and HTL^+ as equivalent to the positive fragment of greatest fixpoint logic. Binders also enhance the expressiveness of guarded team logics because they enable access to information that normally is obscured by the built-in limitations of these logics. We will take a closer look at guarded hybrid team logics and establish a finite model property for the guarded fragment of HTL using model checking games. More precisely, we encode winning strategies of model checking games as relations, a process that is a natural fit for binders. Further, we notice that the hierarchy of guarded team logics is more complex than the hierarchy of non-guarded team logics, and we establish a hierarchy of prominent union-closed guarded team logics.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Team semantics
  • guarded logics
  • expressiveness
  • model checking games


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


  1. Hajnal Andréka, István Németi, and Johan van Benthem. Modal languages and bounded fragments of predicate logic. J. Philos. Log., 27(3):217-274, 1998. URL:
  2. Carlos Areces and Balder ten Cate. Hybrid logics. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 821-868. North-Holland, 2007. URL:
  3. William Ward Armstrong. Dependency structures of data base relationships. In Jack L. Rosenfeld, editor, Information Processing, Proceedings of the 6th IFIP Congress 1974, Stockholm, Sweden, August 5-10, 1974, pages 580-583. North-Holland, 1974. Google Scholar
  4. Vince Bárány, Georg Gottlob, and Martin Otto. Querying the guarded fragment. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, 11-14 July 2010, Edinburgh, United Kingdom, pages 1-10. IEEE Computer Society, 2010. URL:
  5. Vince Bárány, Balder ten Cate, and Luc Segoufin. Guarded negation. In Luca Aceto, Monika Henzinger, and Jirí Sgall, editors, Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II, volume 6756 of Lecture Notes in Computer Science, pages 356-367. Springer, 2011. URL:
  6. Michael Benedikt, Pierre Bourhis, and Michael Vanden Boom. Characterizing definability in decidable fixpoint logics. In Ioannis Chatzigiannakis, Piotr Indyk, Fabian Kuhn, and Anca Muscholl, editors, 44th International Colloquium on Automata, Languages, and Programming, ICALP 2017, July 10-14, 2017, Warsaw, Poland, volume 80 of LIPIcs, pages 107:1-107:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL:
  7. Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. URL:
  8. Patrick Blackburn, Johan van Benthem, and Frank Wolter, editors. Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning. North-Holland, 2007. URL:
  9. Marco A. Casanova, Ronald Fagin, and Christos H. Papadimitriou. Inclusion dependencies and their interaction with functional dependencies. In Jeffrey D. Ullman and Alfred V. Aho, editors, Proceedings of the ACM Symposium on Principles of Database Systems, March 29-31, 1982, Los Angeles, California, USA, pages 171-176. ACM, 1982. URL:
  10. Marco A. Casanova and Vânia Maria Ponte Vidal. Towards a sound view integration methodology. In Ronald Fagin and Philip A. Bernstein, editors, Proceedings of the Second ACM SIGACT-SIGMOD Symposium on Principles of Database Systems, March 21-23, 1983, Colony Square Hotel, Atlanta, Georgia, USA, pages 36-47. ACM, 1983. URL:
  11. Haim Gaifman. On local and non-local properties. In J. Stern, editor, Proceedings of the Herbrand Symposium, volume 107 of Studies in Logic and the Foundations of Mathematics, pages 105-135. Elsevier, 1982. URL:
  12. Pietro Galliani. Inclusion and exclusion dependencies in team semantics - on some logics of imperfect information. Ann. Pure Appl. Log., 163(1):68-84, 2012. URL:
  13. Pietro Galliani and Lauri Hella. Inclusion logic and fixed point logic. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 281-295. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013. URL:
  14. Dan Geiger, Azaria Paz, and Judea Pearl. Axioms and algorithms for inferences involving probabilistic independence. Inf. Comput., 91(1):128-141, 1991. URL:
  15. Valentin Goranko. Temporal logic with reference pointers. In Dov M. Gabbay and Hans Jürgen Ohlbach, editors, Temporal Logic, First International Conference, ICTL '94, Bonn, Germany, July 11-14, 1994, Proceedings, volume 827 of Lecture Notes in Computer Science, pages 133-148. Springer, 1994. URL:
  16. Erich Grädel. On the restraining power of guards. J. Symb. Log., 64(4):1719-1742, 1999. URL:
  17. Erich Grädel, Colin Hirsch, and Martin Otto. Back and forth between guarded and modal logics. ACM Trans. Comput. Log., 3(3):418-463, 2002. URL:
  18. Erich Grädel and Martin Otto. The freedoms of (guarded) bisimulation. In Alexandru Baltag and Sonja Smets, editors, Johan van Benthem on Logic and Information Dynamics, pages 3-31. Springer, 2014. URL:
  19. Erich Grädel and Martin Otto. Guarded teams: The horizontally guarded case. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 22:1-22:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL:
  20. Erich Grädel and Jouko A. Väänänen. Dependence and independence. Stud Logica, 101(2):399-410, 2013. URL:
  21. Jaakko Hintikka and Gabriel Sandu. Informational independence as a semantical phenomenon. In Jens Erik Fenstad, Ivan T. Frolov, and Risto Hilpinen, editors, Logic, Methodology and Philosophy of Science VIII, volume 126 of Studies in Logic and the Foundations of Mathematics, pages 571-589. Elsevier, 1989. URL:
  22. W. Hodges. Compositional semantics for a language of imperfect information. Logic Journal of the IGPL, 5(4):539-563, 1997. URL:
  23. Neil Immerman. Relational queries computable in polynomial time. Inf. Control., 68(1-3):86-104, 1986. URL:
  24. Juha Kontinen and Ville Nurmi. Team logic and second-order logic. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of Lecture Notes in Computer Science, pages 230-241. Springer, 2009. URL:
  25. Juha Kontinen and Jouko A. Väänänen. On definability in dependence logic. J. Log. Lang. Inf., 18(3):317-332, 2009. URL:
  26. Martin Lück. Team logic: axioms, expressiveness, complexity. PhD thesis, University of Hanover, Hannover, Germany, 2020. URL:
  27. Martin Otto. Highly acyclic groups, hypergraph covers, and the guarded fragment. J. ACM, 59(1):5:1-5:40, 2012. URL:
  28. Arthur Prior. Past, Present and Future. Oxford,: Clarendon P., 1967. Google Scholar
  29. Jouko A. Väänänen. Dependence Logic - A New Approach to Independence Friendly Logic, volume 70 of London Mathematical Society student texts. Cambridge University Press, 2007. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail