Document Open Access Logo

Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents

Authors Tim Lyon , Alwen Tiu, Rajeev Goré, Ranald Clouston

PDF
Thumbnail PDF

File

LIPIcs.CSL.2020.28.pdf
  • Filesize: 0.57 MB
  • 16 pages

Document Identifiers

Author Details

Tim Lyon
  • Institut für Logic and Computation, Technische Universität Wien, Austria
Alwen Tiu
  • Research School of Computer Science, The Australian National University, Australia
Rajeev Goré
  • Research School of Computer Science, The Australian National University, Australia
Ranald Clouston
  • Research School of Computer Science, The Australian National University, Australia

Funding

  • Lyon, Tim: Supported by the European Union Horizon 2020 Marie Skłodowska-Curie grant No 689176 and FWF projects I 2982, Y544-N2, and W1255-N23.

Cite As Get BibTex

Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.28

Abstract

We provide a direct method for proving Craig interpolation for a range of modal and intuitionistic logics, including those containing a "converse" modality. We demonstrate this method for classical tense logic, its extensions with path axioms, and for bi-intuitionistic logic. These logics do not have straightforward formalisations in the traditional Gentzen-style sequent calculus, but have all been shown to have cut-free nested sequent calculi. The proof of the interpolation theorem uses these calculi and is purely syntactic, without resorting to embeddings, semantic arguments, or interpreted connectives external to the underlying logical language. A novel feature of our proof includes an orthogonality condition for defining duality between interpolants.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Automated reasoning
Keywords
  • Bi-intuitionistic logic
  • Interpolation
  • Nested calculi
  • Proof theory
  • Sequents
  • Tense logics

Metrics

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

Related Versions

References

  1. Kai Brünnler. Deep sequent systems for modal logic. Arch. Math. Log., 48(6):551-577, 2009. Google Scholar
  2. Agata Ciabattoni, Nikolaos Galatos, and Kazushige Terui. From Axioms to Analytic Rules in Nonclassical Logics. In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 229-240, 2008. URL: https://doi.org/10.1109/LICS.2008.39.
  3. Agata Ciabattoni, Tim Lyon, and Revantha Ramanayake. From Display to Labelled Proofs for Tense Logics. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 120-139, Cham, 2018. Springer International Publishing. Google Scholar
  4. Ranald Clouston, Jeremy E. Dawson, Rajeev Goré, and Alwen Tiu. Annotation-Free Sequent Calculi for Full Intuitionistic Linear Logic. In Computer Science Logic 2013 (CSL 2013), CSL 2013, September 2-5, 2013, Torino, Italy, volume 23 of LIPIcs, pages 197-214. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.197.
  5. Vincent Danos and Laurent Regnier. The structure of multiplicatives. Arch. Math. Log., 28(3):181-203, 1989. URL: https://doi.org/10.1007/BF01622878.
  6. Melvin Fitting and Roman Kuznets. Modal interpolation via nested sequents. Ann. Pure Appl. Logic, 166(3):274-305, 2015. URL: https://doi.org/10.1016/j.apal.2014.11.002.
  7. Rajeev Goré. Substructural Logics on Display. Logic Journal of the IGPL, 6(3):451-504, 1998. Google Scholar
  8. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Advances in Modal Logic 7, papers from the seventh conference on "Advances in Modal Logic," held in Nancy, France, 9-12 September 2008, pages 43-66, 2008. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
  9. Rajeev Goré, Linda Postniece, and Alwen Tiu. On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci., 7(2):2:8, 38, 2011. Google Scholar
  10. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-136, 1994. URL: https://doi.org/10.1007/BF01053026.
  11. Hitoshi Kihara and Hiroakira Ono. Interpolation Properties, Beth Definability Properties and Amalgamation Properties for Substructural Logics. Journal of Logic and Computation, 20(4), August 2010. Google Scholar
  12. Tomasz Kowalski and Hiroakira Ono. Analytic Cut and interpolation for bi-intuitionistic Logic. Rew. Symb. Logic, 10(2):259-283, 2017. URL: https://doi.org/10.1017/S175502031600040X.
  13. Roman Kuznets. Multicomponent proof-theoretic method for proving interpolation properties. Ann. Pure Appl. Logic, 169(12):1369-1418, 2018. Google Scholar
  14. Roman Kuznets and Björn Lellmann. Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents. In Proc. AiML 2018. Kings College Publications, 2018. Google Scholar
  15. Carsten Lutz and Frank Wolter. Foundations for Uniform Interpolation and Forgetting in Expressive Description Logics. In IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, pages 989-995, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-170.
  16. Tim Lyon, Alwen Tiu, Ranald Clouston, and Rajeev Goré. Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents. CoRR, abs/1910, 2019. URL: http://arxiv.org/abs/1910.05215.
  17. S. Maehara. Craig no interpolation theorem (in Japanese). Suugaku, 12:235–237, 1960. Google Scholar
  18. Kenneth L. McMillan. Interpolation and Model Checking. In Handbook of Model Checking, pages 421-446. Springer, 2018. Google Scholar
  19. Sara Negri. Proof Analysis in Modal Logic. J. Philosophical Logic, 34(5-6):507-544, 2005. Google Scholar
  20. Luís Pinto and Tarmo Uustalu. A proof-theoretic study of bi-intuitionistic propositional sequent calculus. J. Log. Comput., 28(1):165-202, 2018. URL: https://doi.org/10.1093/logcom/exx044.
  21. Francesca Poggiolesi. A Cut-Free Simple Sequent Calculus for Modal Logic S5. Rew. Symb. Logic, 1(1):3-15, 2008. URL: https://doi.org/10.1017/S1755020308080040.
  22. Cecylia Rauszer. An algebraic and Kripke-style approach to a certain extension of intuitionistic logic. Instytut Matematyczny Polskiej Akademi Nauk, 1980. URL: http://eudml.org/doc/268511.
  23. Balder ten Cate, Enrico Franconi, and Inanç Seylan. Beth Definability in Expressive Description Logics. J. Artif. Intell. Res., 48:347-414, 2013. Google Scholar
  24. Alwen Tiu, Egor Ianovski, and Rajeev Goré. Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures. In Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012, pages 516-537, 2012 . URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.
  25. Anne Troesltra and Helmut Schwichtenberg. Basic Proof Theory. CUP, 1996. 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