Abstract
Proof theory for a logic with categorical semantics can be developed by the following methodology: define a sound and complete display calculus for an extension of the logic with additional adjunctions; translate this calculus to a shallow inference nested sequent calculus; translate this calculus to a deep inference nested sequent calculus; then prove this final calculus is sound with respect to the original logic. This complex chain of translations between the different calculi require proofs that are technically intricate and involve a large number of cases, and hence are ideal candidates for formalisation. We present a formalisation of this methodology in the case of Full Intuitionistic Linear Logic (FILL), which is multiplicative intuitionistic linear logic extended with par.
Chapter PDF
References
Belnap, N.D.: Display logic. J. Philos. Logic 11, 375–417 (1982)
Bierman, G.M.: A note on full intuitionistic linear logic. Ann. Pure Appl. Logic 79(3), 281–287 (1996)
Bräuner, T., de Paiva, V.: A formulation of linear logic based on dependency-relations. In: Nielsen, M. (ed.) CSL 1997. LNCS, vol. 1414, pp. 129–148. Springer, Heidelberg (1998)
Brünnler, K.: Deep sequent systems for modal logic. Arch. Math. Logic 48(6), 551–577 (2009)
Clouston, R., Dawson, J.E., Goré, R., Tiu, A.: Annotation-free sequent calculi for full intuitionistic linear logic. In: CSL, pp. 197–214 (2013)
Clouston, R., Dawson, J.E., Goré, R., Tiu, A.: Annotation-free sequent calculi for full intuitionistic linear logic - extended version. CoRR, abs/1307.0289 (2013)
Dawson, J.E., Goré, R.P.: Formalised cut admissibility for display logic. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 131–147. Springer, Heidelberg (2002)
Dawson, J.E., Goré, R.: Generic methods for formalising sequent calculi applied to provability logic. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 263–277. Springer, Heidelberg (2010)
Goré, R.: Substructural logics on display. Log. J. IGPL 6(3), 451–504 (1998)
Goré, R., Postniece, L., Tiu, A.: Cut-elimination and proof search for bi-intuitionistic tense logic. In: AiML, pp. 156–177 (2010)
Goré, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. LMCS 7(2) (2011)
Hyland, M., de Paiva, V.: Full intuitionistic linear logic (extended abstract). Ann. Pure Appl. Logic 64(3), 273–291 (1993)
Kashima, R.: Cut-free sequent calculi for some tense logics. Studia Log. 53, 119–135 (1994)
Park, J., Seo, J., Park, S.: A theorem prover for boolean BI. In: POPL 2013, pp. 219–232 (2013)
Poggiolesi, F.: The method of tree-hypersequents for modal propositional logic. In: Trends in Logic IV, pp. 31–51 (2009)
Schellinx, H.: Some syntactical observations on linear logic. J. Logic Comput. 1(4), 537–559 (1991)
Straßburger, L.: Cut elimination in nested sequents for intuitionistic modal logics. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 209–224. Springer, Heidelberg (2013)
Traytel, D., Popescu, A., Blanchette, J.C.: Foundational, compositional (co)datatypes for higher-order logic: Category theory applied to theorem proving. In: LICS, pp. 596–605 (2012)
Urban, C.: Nominal techniques in isabelle/HOL. J. Automat. Reason. 40(4), 327–356 (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Dawson, J.E., Clouston, R., Goré, R., Tiu, A. (2014). From Display Calculi to Deep Nested Sequent Calculi: Formalised for Full Intuitionistic Linear Logic. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds) Theoretical Computer Science. TCS 2014. Lecture Notes in Computer Science, vol 8705. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-44602-7_20
Download citation
DOI: https://doi.org/10.1007/978-3-662-44602-7_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-44601-0
Online ISBN: 978-3-662-44602-7
eBook Packages: Computer ScienceComputer Science (R0)