Document Open Access Logo

A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk)

Author Alwen Tiu

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.2.pdf
  • Filesize: 481 kB
  • 4 pages

Document Identifiers

Author Details

Alwen Tiu
  • School of Computing, The Australian National University, Canberra, Australia

Cite As Get BibTex

Alwen Tiu. A Methodology for Designing Proof Search Calculi for Non-Classical Logics (Invited Talk). In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 2:1-2:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSCD.2022.2

Abstract

In this talk I present a methodology for designing proof search calculi for a wide range of non-classical logics, such as modal and tense logics, bi-intuitionistic (linear) logics and grammar logics. Most of these logics cannot be easily formalised in the traditional Gentzen-style sequent calculus; various structural extensions to sequent calculus seem to be required. One of the more expressive extensions of sequent calculus is Belnap’s display calculus, which allows one to formalise a very wide range of logics and which provides a generic cut-elimination method for logics formalised in the calculus. The generality of display calculus derives partly from the pervasive use of structural rules to capture properties of the underlying semantics of the logic of interest, such as various frame conditions in normal modal logics, that are not easily captured by introduction rules alone. Unlike traditional sequent calculi, the subformula property in display calculi does not typically give an immediate bound on the search space (assuming contraction is absent) in proof search, as new structures may be created and their creation may not be driven by any introduction rules for logical connectives. This line of work started out as an attempt to "tame" display calculus, to make it more proof search friendly, by eliminating or restricting the use of structural rules. Two key ideas that make this possible are the adoption of deep inference, allowing inference rules to be applied inside a nested structure, and the use of propagation rules in place of structural rules. A brief survey of the applications of this methodology to a wide range of logics is presented, along with some directions for future work.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Proof theory
  • Sequent calculus
  • Display calculus
  • Nested sequent calculus
  • Deep inference

Metrics

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

References

  1. Arnon Avron. Hypersequents, logical consequence and intermediate logics for concurrency. Ann. Math. Artif. Intell., 4:225-248, 1991. URL: https://doi.org/10.1007/BF01531058.
  2. Kai Brünnler. Deep sequent systems for modal logic. Arch. Math. Log., 48(6):551-577, 2009. Google Scholar
  3. Agata Ciabattoni, Tim S. Lyon, Revantha Ramanayake, and Alwen Tiu. Display to labeled proofs and back again for tense logics. ACM Trans. Comput. Log., 22(3):20:1-20:31, 2021. URL: https://doi.org/10.1145/3460492.
  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. Melvin Fitting. Nested sequents and prefixed tableaus. In Martin Giese and Roman Kuznets, editors, TABLEAUX 2011 - Workshops, Tutorials, and Short Papers, Bern, Switzerland, July 4-8, 2011, volume IAM-11-002 of Technical Report, page 69, 2011. Google Scholar
  6. Dov M Gabbay. Labelled deductive systems, volume 33 of Oxford Logic guides. Clarendon Press/Oxford Science Publications, 1996. Google Scholar
  7. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents. In Carlos Areces and Robert Goldblatt, editors, 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. College Publications, 2008. URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf.
  8. Rajeev Goré, Linda Postniece, and Alwen Tiu. Taming displayed tense logics using nested sequents with deep inference. In TABLEAUX, volume 5607 of Lecture Notes in Computer Science, pages 189-204. Springer, 2009. Google Scholar
  9. Rajeev Goré, Linda Postniece, and Alwen Tiu. Cut-elimination and proof search for bi-intuitionistic tense logic. In Lev D. Beklemishev, Valentin Goranko, and Valentin B. Shehtman, editors, Advances in Modal Logic 8, papers from the eighth conference on "Advances in Modal Logic," held in Moscow, Russia, 24-27 August 2010, pages 156-177. College Publications, 2010. URL: http://www.aiml.net/volumes/volume8/Gore-Postniece-Tiu.pdf.
  10. 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), 2011. URL: https://doi.org/10.2168/LMCS-7(2:8)2011.
  11. Rajeev Goré and Revantha Ramanayake. Labelled tree sequents, tree hypersequents and nested (deep) sequents. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, Advances in Modal Logic 9, papers from the ninth conference on "Advances in Modal Logic," held in Copenhagen, Denmark, 22-25 August 2012, pages 279-299. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Gore-Ramanayake.pdf.
  12. Alessio Guglielmi. A system of interaction and structure. ACM Trans. Comput. Log., 8(1):1, 2007. URL: https://doi.org/10.1145/1182613.1182614.
  13. Martin Hyland and Valeria de Paiva. Full intuitionistic linear logic (extended abstract). Ann. Pure Appl. Log., 64(3):273-291, 1993. URL: https://doi.org/10.1016/0168-0072(93)90146-5.
  14. Nuel D. Belnap Jr. Display logic. J. Philos. Log., 11(4):375-417, 1982. URL: https://doi.org/10.1007/BF00284976.
  15. Ryo Kashima. Cut-free sequent calculi for some tense logics. Studia Logica, 53(1):119-136, 1994. URL: https://doi.org/10.1007/BF01053026.
  16. Tim Lyon, Alwen Tiu, Rajeev Goré, and Ranald Clouston. Syntactic interpolation for tense logics and bi-intuitionistic logic via nested sequents. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, January 13-16, 2020, Barcelona, Spain, volume 152 of LIPIcs, pages 28:1-28:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.28.
  17. Sara Negri. Proof analysis in modal logic. J. Philos. Log., 34(5-6):507-544, 2005. URL: https://doi.org/10.1007/s10992-005-2267-3.
  18. Luís Pinto and Tarmo Uustalu. Relating sequent calculi for bi-intuitionistic propositional logic. In Steffen van Bakel, Stefano Berardi, and Ulrich Berger, editors, Proceedings Third International Workshop on Classical Logic and Computation, CL&C 2010, Brno, Czech Republic, 21-22 August 2010, volume 47 of EPTCS, pages 57-72, 2010. URL: https://doi.org/10.4204/EPTCS.47.7.
  19. Francesca Poggiolesi. The method of tree-hypersequents for modal propositional logic. In David Makinson, Jacek Malinowski, and Heinrich Wansing, editors, Towards Mathematical Philosophy, volume 28 of Trends in logic, pages 31-51. Springer, 2009. URL: https://doi.org/10.1007/978-1-4020-9084-4_3.
  20. Linda Postniece. Deep inference in bi-intuitionistic logic. In Hiroakira Ono, Makoto Kanazawa, and Ruy J. G. B. de Queiroz, editors, Logic, Language, Information and Computation, 16th International Workshop, WoLLIC 2009, Tokyo, Japan, June 21-24, 2009. Proceedings, volume 5514 of Lecture Notes in Computer Science, pages 320-334. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02261-6_26.
  21. Alwen Tiu, Egor Ianovski, and Rajeev Goré. Grammar logics in nested sequent calculus: Proof theory and decision procedures. In Thomas Bolander, Torben Braüner, Silvio Ghilardi, and Lawrence S. Moss, editors, 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. College Publications, 2012. URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf.
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