Document Open Access Logo

Uniform Interpolation in Coalgebraic Modal Logic

Authors Fatemeh Seifan, Lutz Schröder, Dirk Pattinson

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2017.21.pdf
  • Filesize: 0.51 MB
  • 16 pages

Document Identifiers

Author Details

Fatemeh Seifan
Lutz Schröder
Dirk Pattinson

Cite As Get BibTex

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) https://doi.org/10.4230/LIPIcs.CALCO.2017.21

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.

Subject Classification

Keywords
  • modal logic
  • coalgebraic logic
  • uniform interpolation
  • preservation of weak pullbacks

Metrics

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

References

  1. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and Concrete Categories. Wiley Interscience, 1990. Republished in Reprints in Theor. Appl. Cat. 17 (2006). Google Scholar
  2. Michael Barr. Terminal coalgebras in well-founded set theory. Theoret. Comput. Sci., 114:299-315, 1993. Google Scholar
  3. Marta Bílková. Uniform interpolation and propositional quantifiers in modal logics. Stud. Log., 85:1-31, 2007. Google Scholar
  4. Brian Chellas. Modal Logic. Cambridge University Press, 1980. Google Scholar
  5. William Craig. Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log., 22:250-268, 1957. Google Scholar
  6. Giovanna D'Agostino and Marco Hollenberg. Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski. J. Symb. Log., 65:310-332, 2000. Google Scholar
  7. Stéphane Demri and Denis Lugiez. Complexity of modal logics with Presburger constraints. J. Appl. Log., 8:233-252, 2010. Google Scholar
  8. Dov Gabbay. Craig’s interpolation theorem for modal logics. In Conference in Mathematical Logic—London’70, volume 255 of LNM, pages 111-127. Springer, 1972. Google Scholar
  9. Dov Gabbay. Craig interpolation theorem for intuitionistic logic and extensions Part III. J. Symb. Log., 42:269-271, 1977. Google Scholar
  10. Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Log., 71:189-245, 1995. Google Scholar
  11. Silvio Ghilardi and Marek Zawadowski. Undefinability of propositional quantifiers in the modal system S4. Stud. Log., 55:259-271, 1995. Google Scholar
  12. H. Peter Gumm and Tobias Schröder. Coalgebraic structure from weak limit preserving functors. In Coalgebraic Methods in Computer Science, CMCS 2000, volume 33 of ENTCS, pages 111-131. Elsevier, 2000. Google Scholar
  13. H. Peter Gumm and Tobias Schröder. Monoid-labeled transition systems. In Coalgebraic Methods in Computer Science, CMCS 2001, volume 44 of ENTCS, pages 185-204. Elsevier, 2001. Google Scholar
  14. Helle Hansen and Clemens Kupke. A coalgebraic perspective on monotone modal logic. In Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 121-143. Elsevier, 2004. Google Scholar
  15. Helle Hansen, Clemens Kupke, and Eric Pacuit. Neighbourhood structures: Bisimilarity and basic model theory. Log. Meth. Comput. Sci., 5, 2009. Google Scholar
  16. Leon Henkin. An extension of the Craig-Lyndon interpolation theorem. J. Symb. Log., 28:201-216, 1963. Google Scholar
  17. Dexter Kozen. Results on the propositional μ-calculus. Theor. Comput. Sci., 27:333-354, 1983. Google Scholar
  18. Alexander Kurz and Raul Leal. Modalities in the Stone age: A comparison of coalgebraic logics. Theor. Comput. Sci., 430:88-116, 2012. URL: http://dx.doi.org/10.1016/j.tcs.2012.03.027,
  19. Carsten Lutz and Frank Wolter. Foundations for uniform interpolation and forgetting in expressive description logics. In International Joint Conference on Artificial Intelligence, IJCAI 2011, pages 989-995. IJCAI/AAAI, 2011. Google Scholar
  20. Johannes Marti. Relation liftings in coalgebraic modal logic. Master’s thesis, Universiteit van Amsterdam, 2011. Google Scholar
  21. Johannes Marti, Fatemeh Seifan, and Yde Venema. Uniform interpolation for coalgebraic fixpoint logic. In Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 238-252. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  22. Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81:880-900, 2015. Google Scholar
  23. Larry Moss. Coalgebraic logic. Ann. Pure Appl. Logic, 96:277-317, 1999. Google Scholar
  24. Rob Myers, Dirk Pattinson, and Lutz Schröder. Coalgebraic hybrid logic. In Foundations of Software Science and Computation Structures, FoSSaCS 2009, volume 5504 of LNCS, pages 137-151. Springer, 2009. Google Scholar
  25. Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoret. Comput. Sci., 309:177-193, 2003. Google Scholar
  26. Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log., 45:19-33, 2004. Google Scholar
  27. Dirk Pattinson. The logic of exact covers: Completeness and uniform interpolation. In Logic in Computer Science, LICS 2013, pages 418-427. IEEE, 2013. Google Scholar
  28. Dirk Pattinson and Lutz Schröder. Cut elimination in coalgebraic logics. Inf. Comput., 208:1447-1468, 2010. Google Scholar
  29. Marc Pauly. A modal logic for coalitional power in games. J. Log. Comput., 12:149-166, 2002. Google Scholar
  30. Andrew Pitts. On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Log., 57:33-52, 1992. Google Scholar
  31. Jan Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  32. Luigi Santocanale and Yde Venema. Uniform interpolation for monotone modal logic. In Advances in Modal Logic, AiML 2010, pages 350-370. College Publications, 2010. Google Scholar
  33. Lutz Schröder. A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog., 73:97-110, 2007. Google Scholar
  34. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390:230-247, 2008. Google Scholar
  35. Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Symposium on Theoretical Aspects of Computer Science, STACS 2009, volume 3 of LIPIcs, pages 673-684. Schloss Dagstuhl - Leibniz-Center of Informatics, 2009. Google Scholar
  36. Lutz Schröder and Dirk Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20(5):1113-1147, 2010. Google Scholar
  37. Daniele Turi. Functorial operational semantics and its denotational dual. PhD thesis, Vrije Universiteit, Amsterdam, 1996. Google Scholar
  38. Albert Visser. Uniform interpolation and layered bisimulation. In Gödel ’96 (Brno, 1996), volume 6 of Lect. Notes Log., pages 139-164. Springer, 1996. Google Scholar
  39. Kewen Wang, Zhe Wang, Rodney Topor, Jeff Pan, and Grigoris Antoniou. Concept and role forgetting in ALC-ontologies. In The Semantic Web, ISWC 2009, volume 5823 of LNCS. Springer, 2009. Google Scholar
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 About DROPS Imprint Privacy Contact