LIPIcs.CSL.2020.25.pdf
- Filesize: 0.54 MB
- 16 pages
Document
On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics
Authors
-
Part of:
Volume:
28th EACSL Annual Conference on Computer Science Logic (CSL 2020)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Computer Science Logic (CSL) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2020-01-06
Cite AsGet BibTex
Matthias Hoelzel and Richard Wilke. On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 25:1-25:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.CSL.2020.25
https://doi.org/10.4230/LIPIcs.CSL.2020.25
Abstract
We present syntactic characterisations for the union closed fragments of existential second-order logic and of logics with team semantics. Since union closure is a semantical and undecidable property, the normal form we introduce enables the handling and provides a better understanding of this fragment. We also introduce inclusion-exclusion games that turn out to be precisely the corresponding model-checking games. These games are not only interesting in their own right, but they also are a key factor towards building a bridge between the semantic and syntactic fragments. On the level of logics with team semantics we additionally present restrictions of inclusion-exclusion logic to capture the union closed fragment. Moreover, we define a team based atom that when adding it to first-order logic also precisely captures the union closed fragment of existential second-order logic which answers an open question by Galliani and Hella.
Subject Classification
ACM Subject Classification
- Theory of computation → Higher order logic
Keywords
- Higher order logic
- Existential second-order logic
- Team semantics
- Closure properties
- Union closure
- Model-checking games
- Syntactic charactisations of semantical fragments
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Pietro Galliani. Inclusion and Exclusion Dependencies in Team Semantics - on Some Logics of Imperfect Information. Annals of Pure and Applied Logic, 163(1):68-84, 2012.
- Pietro Galliani and Lauri Hella. Inclusion Logic and Fixed Point Logic. In Simona Ronchi Della Rocca, editor, Computer Science Logic 2013 (CSL 2013), volume 23 of Leibniz International Proceedings in Informatics (LIPIcs), pages 281-295, Dagstuhl, Germany, 2013. Schloss Dagstuhl-Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.281.
-
Erich Grädel. Games for Inclusion Logic and Fixed-Point Logic. In Samson Abramsky and Others, editors, Dependence Logic: Theory and Applications, pages 73-98. Birkhäuser, 2016.
-
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. Springer-Verlag, Berlin Heidelberg, 2007.
- Erich Grädel and Jouko Väänänen. Dependence and Independence. Studia Logica, 101(2):399-410, 2013. URL: https://doi.org/10.1007/s11225-013-9479-2.
-
Wilfrid Hodges. A Shorter Model Theory. Cambridge University Press, New York, NY, USA, 1997.
- Wilfrid Hodges. Compositional Semantics for a Language of Imperfect Information. Logic Journal of the IGPL, 5(4):539-563, 1997. URL: https://doi.org/10.1093/jigpal/5.4.539.
-
Juha Kontinen and Jouko Väänänen. On Definability in Dependence Logic. Journal of Logic, Language and Information, 18(3):317-332, 2009.
-
Jouko Väänänen. Dependence Logic: A New Approach to Independence Friendly Logic (London Mathematical Society Student Texts). Cambridge University Press, New York, NY, USA, 2007.
-
Johan van Benthem. Modal Correspondence Theory. PhD dissertation, University of Amsterdam, 1976.