DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2020.25

On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics

Authors: Matthias Hoelzel and Richard Wilke

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{hoelzel_et_al:LIPIcs.CSL.2020.25,
  author =	{Hoelzel, Matthias and Wilke, Richard},
  title =	{{On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{25:1--25:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.25},
  URN =		{urn:nbn:de:0030-drops-116681},
  doi =		{10.4230/LIPIcs.CSL.2020.25},
  annote =	{Keywords: Higher order logic, Existential second-order logic, Team semantics, Closure properties, Union closure, Model-checking games, Syntactic charactisations of semantical fragments}
}

Document

DOI: 10.4230/LIPIcs.CSL.2018.25

Dependency Concepts up to Equivalence

Authors: Erich Grädel and Matthias Hoelzel

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract

Modern logics of dependence and independence are based on different variants of atomic dependency statements (such as dependence, exclusion, inclusion, or independence) and on team semantics: A formula is evaluated not with a single assignment of values to the free variables, but with a set of such assignments, called a team. In this paper we explore logics of dependence and independence where the atomic dependency statements cannot distinguish elements up to equality, but only up to a given equivalence relation (which may model observational indistinguishabilities, for instance between states of a computational process or between values obtained in an experiment). Our main goal is to analyse the power of such logics, by identifying equally expressive fragments of existential second-order logic or greatest fixed-point logic, with relations that are closed under the given equivalence. Using an adaptation of the Ehrenfeucht-Fraïssé method we further study conditions on the given equivalences under which these logics collapse to first-order logic, are equivalent to full existential second-order logic, or are strictly between first-order and existential second-order logic.

Cite as

Erich Grädel and Matthias Hoelzel. Dependency Concepts up to Equivalence. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gradel_et_al:LIPIcs.CSL.2018.25,
  author =	{Gr\"{a}del, Erich and Hoelzel, Matthias},
  title =	{{Dependency Concepts up to Equivalence}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{25:1--25:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.25},
  URN =		{urn:nbn:de:0030-drops-96921},
  doi =		{10.4230/LIPIcs.CSL.2018.25},
  annote =	{Keywords: Logics of dependence and independence, Team semantics, Existential second-order logic, Observational equivalence, Expressive power}
}

Search Results

Documents authored by Hoelzel, Matthias

On the Union Closed Fragment of Existential Second-Order Logic and Logics with Team Semantics

Abstract

Cite as

Dependency Concepts up to Equivalence

Abstract

Cite as

Thanks for your feedback!

Could not send message