3 Search Results for "Seifan, Fatemeh"

Document
DOI: 10.4230/LIPIcs.CALCO.2017.21
Uniform Interpolation in Coalgebraic Modal Logic

Authors: Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson

Published in: LIPIcs, Volume 72, 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)

Abstract
A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula - the interpolant - to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
Cite as

Fatemeh Seifan, Lutz Schröder, and Dirk Pattinson. Uniform Interpolation in Coalgebraic Modal Logic. In 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 72, pp. 21:1-21:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{seifan_et_al:LIPIcs.CALCO.2017.21,
  author =	{Seifan, Fatemeh and Schr\"{o}der, Lutz and Pattinson, Dirk},
  title =	{{Uniform Interpolation in Coalgebraic Modal Logic}},
  booktitle =	{7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017)},
  pages =	{21:1--21:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-033-0},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{72},
  editor =	{Bonchi, Filippo and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2017.21},
  URN =		{urn:nbn:de:0030-drops-80415},
  doi =		{10.4230/LIPIcs.CALCO.2017.21},
  annote =	{Keywords: modal logic, coalgebraic logic, uniform interpolation, preservation of weak pullbacks}
}
Document
DOI: 10.4230/LIPIcs.CSL.2016.7
Completeness for Coalgebraic Fixpoint Logic

Authors: Sebastian Enqvist, Fatemeh Seifan, and Yde Venema

Published in: LIPIcs, Volume 62, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016)

Abstract
We introduce an axiomatization for the coalgebraic fixed point logic which was introduced by Venema as a generalization, based on Moss' coalgebraic modality, of the well-known modal mu-calculus. Our axiomatization can be seen as a generalization of Kozen's proof system for the modal mu-calculus to the coalgebraic level of generality. It consists of a complete axiomatization for Moss'modality, extended with Kozen's axiom and rule for the fixpoint operators. Our main result is a completeness theorem stating that, for functors that preserve weak pullbacks and restrict to finite sets, our axiomatization is sound and complete for the standard interpretation of the language in coalgebraic models. Our proof is based on automata-theoretic ideas: in particular, we introduce the notion of consequence game for modal automata, which plays a crucial role in the proof of our main result. The result generalizes the celebrated Kozen-Walukiewicz completeness theorem for the modal mu-calculus, and our automata-theoretic methods simplify parts of Walukiewicz' proof.
Cite as

Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Completeness for Coalgebraic Fixpoint Logic. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 62, pp. 7:1-7:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{enqvist_et_al:LIPIcs.CSL.2016.7,
  author =	{Enqvist, Sebastian and Seifan, Fatemeh and Venema, Yde},
  title =	{{Completeness for Coalgebraic Fixpoint Logic}},
  booktitle =	{25th EACSL Annual Conference on Computer Science Logic (CSL 2016)},
  pages =	{7:1--7:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-022-4},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{62},
  editor =	{Talbot, Jean-Marc and Regnier, Laurent},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2016.7},
  URN =		{urn:nbn:de:0030-drops-65470},
  doi =		{10.4230/LIPIcs.CSL.2016.7},
  annote =	{Keywords: mu-calculus, coalgebra, coalgebraic modal logic, automata, completeness}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.238
Uniform Interpolation for Coalgebraic Fixpoint Logic

Authors: Johannes Marti, Fatemeh Seifan, and Yde Venema

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
We use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoys uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e., functors with quasifunctorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.
Cite as

Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform Interpolation for Coalgebraic Fixpoint Logic. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 238-252, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{marti_et_al:LIPIcs.CALCO.2015.238,
  author =	{Marti, Johannes and Seifan, Fatemeh and Venema, Yde},
  title =	{{Uniform Interpolation for Coalgebraic Fixpoint Logic}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{238--252},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.238},
  URN =		{urn:nbn:de:0030-drops-55379},
  doi =		{10.4230/LIPIcs.CALCO.2015.238},
  annote =	{Keywords: mu-calculus, uniform interpolation, coalgebra, automata}
}
  • Refine by Author
  • 3 Seifan, Fatemeh
  • 2 Venema, Yde
  • 1 Enqvist, Sebastian
  • 1 Marti, Johannes
  • 1 Pattinson, Dirk
  • Show More...

  • Refine by Classification

  • Refine by Keyword
  • 2 automata
  • 2 coalgebra
  • 2 mu-calculus
  • 2 uniform interpolation
  • 1 coalgebraic logic
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2015
  • 1 2016
  • 1 2017

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact