Skip to main content
SpringerLink
Log in

A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi

  • Conference paper
Logic, Language, and Computation (TbiLLC 2009)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 6618))

Included in the following conference series:

Abstract

This paper answers one rather particular question: how to perform a proof of uniform interpolation property in deep inference calculi for modal logics. We show how to perform a proof of uniform interpolation property in deep inference calculus for the basic modal logic K via forgetting a variable in a certain normal form constructed by backward proof search. For that purpose we modify the framework of deep-inference calculus using a cover modality on the meta level to structure deep sequents.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Bílková, M.: Interpolation in Modal Logic. PhD thesis, Charles University in Prague (2006)

    Google Scholar 

  2. Bílková, M.: Uniform interpolation and propositional quantifiers in modal logics. Studia Logica 85(1), 1–31 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  3. Bílková, M., Palmigiano, A., Venema, Y.: Proof systems for the coalgebraic cover modality. In: Areces, C., Goldblatt, R. (eds.) Advances in Modal Logic, vol. 7, pp. 1–21. College Publications (2008)

    Google Scholar 

  4. Brünnler, K.: Deep sequent systems for modal logic. In: Governatori, G., Hodkinson, I., Venema, Y. (eds.) Advances in Modal Logic, vol. 6, pp. 107–120. College Publications (2006)

    Google Scholar 

  5. Brünnler, K., Straßburger, L.: Modular Sequent Systems for Modal Logic. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 152–166. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Brünnler, K.: Deep Sequent Systems for Modal Logic. Archive for Mathematical Logic 48, 551–577 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. ten Cate, B., et al.: Definitorially complete description logics. In: [8], pp. 79–89 (2006)

    Google Scholar 

  8. ten Cate, B., Zeevat, H. (eds.): Logic, Language, and Computation, 6th International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC 2005, Batumi, Georgia, September 12-16, 2005. Revised Selected Papers, Batumi, Georgia, September 12-16. LNCS, vol. 4363, pp. 973–978. Springer, Heidelberg (2007) ISBN 978-3-540-75143-4

    MATH  Google Scholar 

  9. D’Agostino, G.: Uniform interpolation, bisimulation quantifiers, and fixed points. In: [8], pp. 96–116 (2005)

    Google Scholar 

  10. Ghilardi, S., Zawadovski, M.: Undefinability of propositional quantifiers in the modal system S4. Studia Logica 55, 259–271 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  11. Guglielmi, A.: Deep inference and the calculus of structures (2008), Web site at http://alessio.guglielmi.name/res/cos

  12. Hájek, P., Wiedermann, J. (eds.): MFCS 1995. LNCS, vol. 969, pp. 3–540. Springer, Heidelberg (1995) ISBN 3-540-60246-1

    Google Scholar 

  13. Heuerding, A.: Sequent Calculi for Proof Search in Some Modal Logics. PhD thesis, University of Bern, Switzerland (1998)

    Google Scholar 

  14. Heuerding, A., Seyfried, M., Zimmermann, H.: Efficient loop-check for backward proof search in some non-classical propositional logics. Tableaux, 210–225 (1996)

    Google Scholar 

  15. Janin, D., Walukiewicz, I.: Automata for the modal mu-calculus and related results. In: [21], pp. 552–562 (1995)

    Google Scholar 

  16. Negri, S.: Proof analysis in modal logic. Journal of Philosophical Logic 34(5-6), 507–544 (2005)

    Article  MathSciNet  MATH  Google Scholar 

  17. Palmigiano, A., Venema, Y.: Nabla algebras and chu spaces. In: Mossakowski, T., Montanari, U., Haveraaen, M. (eds.) CALCO 2007. LNCS, vol. 4624, pp. 394–408. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Pitts, A.: On an interpretation of second order quantification in first order intuitionistic propositional logic. The Journal of Symbolic Logic 57, 33–52 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  19. Venema, Y.: Algebras and coalgebras. In: van Benthem, J., Blackburn, P., Wolter, F. (eds.) Handbook of Modal Logic, Elsevier, Amsterdam (2006)

    Google Scholar 

  20. Visser, A.: Bisimulations, model descriptions and propositional quantifiers. In: Logic Group Preprint Series, vol. 161. Utrecht University (1996)

    Google Scholar 

  21. Wansing, H.: Sequent proof systems for modal logics. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 8, Kluwer Academic Publishers, Dordrecht (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science AS CR, Pod Vodárenskou věží 2, 182 07, Prague 8, Czech Republic

    Marta Bílková

Authors
  1. Marta Bílková
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computing, Imperial College London, 180 Queen’s Gate, SW7 2AZ, London, UK

    Nick Bezhanishvili

  2. Institute of Language and Information, Department of General Linguistics, Heinrich-Heine-University, Universitätsstraße 1, 40225, Düsseldorf, Germany

    Sebastian Löbner

  3. Zentrum für Allgemeine Sprachwissenschaft, Schützenstraße 18, 10117, Berlin, Germany

    Kerstin Schwabe

  4. Dipartimento di Matematica, via Ponte don Melillo, 84084, Fisciano, (SA), Italy

    Luca Spada

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Bílková, M. (2011). A Note on Uniform Interpolation Proofs in Modal Deep Inference Calculi. In: Bezhanishvili, N., Löbner, S., Schwabe, K., Spada, L. (eds) Logic, Language, and Computation. TbiLLC 2009. Lecture Notes in Computer Science(), vol 6618. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22303-7_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-22303-7_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-22302-0

  • Online ISBN: 978-3-642-22303-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation