Internal and External Calculi: Ordering the Jungle without Being Lost in Translations

Tim S. Lyon; Agata Ciabattoni; Didier Galmiche; Marianna Girlando; Dominique Larchey-Wendling; Daniel Méry; Nicola Olivetti; Revantha Ramanayake

doi:10.18778/0138-0680.2025.02

Authors

Tim S. Lyon Technische Universität Dresden Author https://orcid.org/0000-0003-3214-0828
Agata Ciabattoni Vienna University of Technology, Austria Author https://orcid.org/0000-0001-6947-8772
Didier Galmiche Université de Lorraine, CNRS, LORIA, France Author https://orcid.org/0000-0002-9968-5323
Marianna Girlando University of Amsterdam, Netherlands Author https://orcid.org/0000-0002-9384-1356
Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA, France Author https://orcid.org/0000-0001-9860-7203
Daniel Méry Université de Lorraine, CNRS, LORIA, France Author https://orcid.org/0000-0002-1886-2106
Nicola Olivetti Aix-Marseille University, France Author https://orcid.org/0000-0001-6254-3754
Revantha Ramanayake University of Groningen, Netherlands Author https://orcid.org/0000-0002-7940-9065

DOI:

https://doi.org/10.18778/0138-0680.2025.02

Keywords:

Bunched implication, Conditional logic, Display calculus, External calculus, Hypersequent, Internal calculus, Intuitionistic logic, Labeled calculus, Modal logic, Nested calculus, Proof theory, Sequent, Tense logic

Abstract

This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively straightforward while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between ‘internal calculi’ and ‘external calculi.’ We discuss the ambiguities involved in the informal definitions of these categories, and we critically assess the properties that (calculi from) these classes are purported to possess.

References

A. Avron, A Constructive Analysis of RM, The Journal of Symbolic Logic, vol. 52(4) (1987), pp. 939–951, DOI: https://doi.org/10.2307/2273828 DOI: https://doi.org/10.2307/2273828

A. Avron, The Method of Hypersequents in the Proof Theory of Propositional Non-Classical Logics, [in:] W. Hodges, M. Hyland, C. Steinhorn, J. Truss (eds.), Logic: From Foundations to Applications: European Logic Colloquium, Clarendon Press, USA (1996), p. 1–32. DOI: https://doi.org/10.1093/oso/9780198538622.003.0001

S. Baratella, A. Masini, An approach to infinitary temporal proof theory,Archive for Mathematical Logic, vol. 43(8) (2004), pp. 965–990, DOI: https://doi.org/10.1007/s00153-004-0237-z DOI: https://doi.org/10.1007/s00153-004-0237-z

K. Bednarska, A. Indrzejczak, Hypersequent Calculi for S5: The Methods of Cut Elimination, Logic and Logical Philosophy, vol. 24(3) (2015), pp. 277–311, DOI: https://doi.org/10.12775/LLP.2015.018 DOI: https://doi.org/10.12775/LLP.2015.018

N. D. Belnap, Display logic, Journal of Philosophical Logic, vol. 11(4) (1982), pp. 375–417, DOI: https://doi.org/10.1007/BF00284976 DOI: https://doi.org/10.1007/BF00284976

P. Blackburn, M. de Rijke, Y. Venema, Modal Logic, vol. 53 of Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2001), DOI: https://doi.org/10.1017/CBO9781107050884 DOI: https://doi.org/10.1017/CBO9781107050884

B. Boretti, Proof Analysis in Temporal Logic, Ph.D. thesis, University of Milan (2008).

T. Braüner, Hybrid Logic and its Proof-Theory, vol. 37 of Applied Logic Series, Springer Dordrecht (2011), DOI: https://doi.org/10.1007/978-94-007-0002-4 DOI: https://doi.org/10.1007/978-94-007-0002-4

J. Brotherston, Bunched Logics Displayed, Studia Logica, vol. 100(6) (2012), p. 1223–1254, DOI: https://doi.org/10.1007/s11225-012-9449-0 DOI: https://doi.org/10.1007/s11225-012-9449-0

J. Brotherston, R. Goré, Craig Interpolation in Displayable Logics, [in:] K. Brünnler, G. Metcalfe (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer, Berlin-Heidelberg (2011), pp. 88–103, DOI: https://doi.org/10.1007/978-3-642-22119-4_9 DOI: https://doi.org/10.1007/978-3-642-22119-4_9

K. Brünnler, Deep sequent systems for modal logic, Archive of Mathematical Logic, vol. 48(6) (2009), pp. 551–577, DOI: https://doi.org/10.1007/s00153-009-0137-3 DOI: https://doi.org/10.1007/s00153-009-0137-3

L. Buisman, R. Goré, A Cut-Free Sequent Calculus for Bi-intuitionistic Logic, [in:] N. Olivetti (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer, Berlin-Heidelberg (2007), pp. 90–106, DOI: https://doi.org/10.1007/978-3-540-73099-6_9 DOI: https://doi.org/10.1007/978-3-540-73099-6_9

R. A. Bull, Cut elimination for propositional dynamic logic without *,Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, vol. 38(2) (1992), pp. 85–100, DOI: https://doi.org/10.1002/malq.19920380107 DOI: https://doi.org/10.1002/malq.19920380107

S. R. Buss, An introduction to proof theory, Handbook of Proof Theory, vol. 137 (1998), pp. 1–78. DOI: https://doi.org/10.1016/S0049-237X(98)80016-5

C. Castellini, A. Smaill, A systematic presentation of quantified modal logics, Logic Journal of the IGPL, vol. 10(6) (2002), pp. 571–599, DOI: https://doi.org/10.1093/jigpal/10.6.571 DOI: https://doi.org/10.1093/jigpal/10.6.571

M. A. Castilho, L. F. del Cerro, O. Gasquet, A. Herzig, Modal tableaux with propagation rules and structural rules, Fundamenta Informaticae, vol. 32(3, 4) (1997), pp. 281–297, DOI: https://doi.org/10.3233/FI-1997-323404 DOI: https://doi.org/10.3233/FI-1997-323404

K. Chaudhuri, N. Guenot, L. Strassburger, The Focused Calculus of Structures, [in:] M. Bezem (ed.), 20th EACSL Annual Conference on Computer Science Logic, vol. 12 of Leibniz International Proceedings in Informatics (LIPIcs), Bergen, Norway (2011), pp. 159–173, DOI: https://doi.org/10.4230/LIPIcs.CSL.2011.159

A. Ciabattoni, N. Galatos, K. Terui, From Axioms to Analytic Rules in Nonclassical Logics, [in:] 2008 23rd Annual IEEE Symposium on Logic in Computer Science (2008), pp. 229–240, DOI: https://doi.org/10.1109/LICS.2008.39 DOI: https://doi.org/10.1109/LICS.2008.39

A. Ciabattoni, T. S. Lyon, R. Ramanayake, From Display to Labelled Proofs for Tense Logics, [in:] S. N. Artëmov, A. Nerode (eds.), Logical Foundations of Computer Science – International Symposium, LFCS 2018, vol. 10703 of Lecture Notes in Computer Science, Springer (2018), pp. 120–139, DOI: https://doi.org/10.1007/978-3-319-72056-2_8 DOI: https://doi.org/10.1007/978-3-319-72056-2_8

A. Ciabattoni, T. S. Lyon, R. Ramanayake, A. Tiu, Display to Labeled Proofs and Back Again for Tense Logics, ACM Transactions in Computational Logic, vol. 22(3) (2021), DOI: https://doi.org/10.1145/3460492 DOI: https://doi.org/10.1145/3460492

A. Ciabattoni, P. Maffezioli, L. Spendier, Hypersequent and Labelled Calculi for Intermediate Logics, [in:] D. Galmiche, D. Larchey-Wendling (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 8123 of Lecture Notes in Computer Science, Springer, Berlin-Heidelberg (2013), pp. 81–96, DOI: https://doi.org/10.1007/978-3-642-40537-2_9 DOI: https://doi.org/10.1007/978-3-642-40537-2_9

A. Ciabattoni, R. Ramanayake, Power and Limits of Structural Display Rules, ACM Transactions on Computational Logic, vol. 17(3) (2016), DOI: https://doi.org/10.1145/2874775 DOI: https://doi.org/10.1145/2874775

A. Ciabattoni, R. Ramanayake, Bunched Hypersequent Calculi for Distributive Substructural Logics, [in:] T. Eiter, D. Sands (eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7–12, 2017, vol. 46 of EPiC Series in Computing, EasyChair (2017), pp. 417–434, DOI: https://doi.org/10.29007/ngp3 DOI: https://doi.org/10.29007/ngp3

A. Ciabattoni, L. Straßburger, K. Terui, Expanding the Realm of Systematic Proof Theory, [in:] E. Grädel, R. Kahle (eds.), Computer Science Logic, 23rd international Workshop, CSL 2009, 18th Annual Conference of the EACSL, Coimbra, Portugal, September 7–11, 2009, vol. 5771 of Lecture Notes in Computer Science, Springer (2009), pp. 163–178, DOI: https://doi.org/10.1007/978-3-642-04027-6_14 DOI: https://doi.org/10.1007/978-3-642-04027-6_14

T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel, Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity, Journal of Logic and Computation, vol. 31(1) (2020), pp. 67–111, DOI: https://doi.org/10.1093/logcom/exaa072 DOI: https://doi.org/10.1093/logcom/exaa072

K. Došen, Sequent-systems and groupoid models. I, Studia Logica, vol. 47(4) (1988), pp. 353–385, DOI: https://doi.org/10.1007/BF00671566 DOI: https://doi.org/10.1007/BF00671566

M. Dunn, A ’Gentzen’ system for positive relevant implication, The Journal of Symbolic Logic, vol. 38 (1974), pp. 356–357.

R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic, The Journal of Symbolic Logic, vol. 57(3) (1992), pp. 795–807, DOI: https://doi.org/10.2307/2275431 DOI: https://doi.org/10.2307/2275431

R. Dyckhoff, Intuitionistic decision procedures since Gentzen, Advances in Proof Theory, (2016), pp. 245–267. DOI: https://doi.org/10.1007/978-3-319-29198-7_6

R. Dyckhoff, S. Negri, Proof analysis in intermediate logics, Archive for Mathematical Logic, vol. 51(1–2) (2012), pp. 71–92, DOI: https://doi.org/10.1007/s00153-011-0254-7 DOI: https://doi.org/10.1007/s00153-011-0254-7

M. Fitting, Tableau methods of proof for modal logics, Notre Dame Journal of Formal Logic, vol. 13(2) (1972), pp. 237–247. DOI: https://doi.org/10.1305/ndjfl/1093894722

M. Fitting, Nested Sequents for Intuitionistic Logics, Notre Dame Journal of Formal Logic, vol. 55(1) (2014), pp. 41–61, DOI: https://doi.org/10.1215/00294527-2377869 DOI: https://doi.org/10.1215/00294527-2377869

M. Fitting, R. Kuznets, Modal interpolation via nested sequents, Annals of Pure and Applied Logic, vol. 166(3) (2015), pp. 274–305, DOI: https://doi.org/10.1016/j.apal.2014.11.002 DOI: https://doi.org/10.1016/j.apal.2014.11.002

D. Galmiche, M. Marti, D. Méry, Relating Labelled and Label-Free Bunched Calculi in BI Logic, [in:] 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2019, vol. 11714, Springer, Londres, United Kingdom (2019), pp. 130–146, DOI: https://doi.org/10.1007/978-3-030-29026-9_8 DOI: https://doi.org/10.1007/978-3-030-29026-9_8

D. Galmiche, D. Méry, D. Pym, The Semantics of BI and Resource Tableaux, Mathematical Structures in Computer Science, vol. 15(6) (2005), pp. 1033–1088, DOI: https://doi.org/10.1017/S0960129505004858 DOI: https://doi.org/10.1017/S0960129505004858

D. Galmiche, Y. Salhi, Tree-sequent calculi and decision procedures for intuitionistic modal logics, Journal of Logic and Computation, vol. 28(5) (2018), pp. 967–989, DOI: https://doi.org/https://doi.org/10.1093/logcom/exv039 DOI: https://doi.org/10.1093/logcom/exv039

G. Gentzen, Untersuchungen über das logische Schließen. I, Mathematische zeitschrift, vol. 39(1) (1935), pp. 176–210. DOI: https://doi.org/10.1007/BF01201353

G. Gentzen, Untersuchungen über das logische Schließen. II, Mathematische Zeitschrift, vol. 39(1) (1935), pp. 405–431. DOI: https://doi.org/10.1007/BF01201363

J.-Y. Girard, Linear logic, Theoretical Computer Science, vol. 50(1) (1987), pp. 1–101, DOI: https://doi.org/10.1016/0304-3975(87)90045-4 DOI: https://doi.org/10.1016/0304-3975(87)90045-4

M. Girlando, B. Lellmann, N. Olivetti, G. L. Pozzato, Standard Sequent Calculi for Lewis’ Logics of Counterfactuals, [in:] L. Michael, A. C. Kakas (eds.), Logics in Artificial Intelligence – 15th European Conference, JELIA, vol. 10021 of Lecture Notes in Computer Science (2016), pp. 272–287, DOI: https://doi.org/10.1007/978-3-319-48758-8_18 DOI: https://doi.org/10.1007/978-3-319-48758-8_18

M. Girlando, N. Olivetti, S. Negri, Counterfactual Logic: Labelled and Internal Calculi, Two Sides of the Same Coin?, [in:] G. Bezhanishvili, G. D’Agostino, G. Metcalfe, T. Studer (eds.), Advances in Modal Logic 12, College Publications (2018), pp. 291–310, URL: http://www.aiml.net/volumes/volume12/Girlando-Olivetti-Negri.pdf

R. Goré, B. Lellmann, Syntactic Cut-Elimination and Backward Proof-Search for Tense Logic via Linear Nested Sequents, [in:] S. Cerrito, A. Popescu (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer International Publishing, Cham (2019), pp. 185–202, DOI: https://doi.org/10.1007/978-3-030-29026-9_11 DOI: https://doi.org/10.1007/978-3-030-29026-9_11

R. Goré, L. Postniece, A. Tiu, Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents, [in:] C. Areces, R. Goldblatt (eds.), Advances in Modal Logic 7, College Publications (2008), pp. 43–66, URL: http://www.aiml.net/volumes/volume7/Gore-Postniece-Tiu.pdf

R. Goré, L. Postniece, A. Tiu, On the Correspondence between Display Postulates and Deep Inference in Nested Sequent Calculi for Tense Logics,Logical Methods in Computer Science, vol. 7(2) (2011), DOI: https://doi.org/10.2168/LMCS-7(2:8)2011. DOI: https://doi.org/10.2168/LMCS-7(2:8)2011

R. Goré, Substructural logics on display, Logic Journal of the IGPL, vol. 6(3) (1998), pp. 451–504, DOI: https://doi.org/10.1093/jigpal/6.3.451 DOI: https://doi.org/10.1093/jigpal/6.3.451

G. Greco, M. Ma, A. Palmigiano, A. Tzimoulis, Z. Zhao, Unified correspondence as a proof-theoretic tool, Journal of Logic and Computation, vol. 28(7) (2018), pp. 1367–1442, DOI: https://doi.org/10.1093/logcom/exw022 DOI: https://doi.org/10.1093/logcom/exw022

A. Guglielmi, A System of Interaction and Structure, ACM Transactions on Computational Logic, vol. 8(1) (2007), p. 1–es, DOI: https://doi.org/10.1145/1182613.1182614 DOI: https://doi.org/10.1145/1182613.1182614

R. Hein, Geometric theories and proof theory of modal logic, Master’s thesis, Technische Universität Dresden (2005).

A. Heyting, Die formalen Regeln der intuitionistischen Logik, Sitzungsbericht PreuBische Akademie der Wissenschaften Berlin, physikalisch-mathematische Klasse II, (1930), pp. 42–56.

I. Horrocks, U. Sattler, Decidability of SHIQ with complex role inclusion axioms, Artificial Intelligence, vol. 160(1–2) (2004), pp. 79–104, DOI: https://doi.org/10.1016/j.artint.2004.06.002 DOI: https://doi.org/10.1016/j.artint.2004.06.002

A. Indrzejczak, Linear Time in Hypersequent Framework, The Bulletin of Symbolic Logic, vol. 22(1) (2016), pp. 121–144, DOI: https://doi.org/10.1017/bsl.2016.2 DOI: https://doi.org/10.1017/bsl.2016.2

A. Indrzejczak, Cut elimination in Hypersequent Calculus for some Logics of Linear Time, The Review of Symbolic Logic, vol. 12(4) (2019), pp. 806–822, DOI: https://doi.org/10.1017/S1755020319000352 DOI: https://doi.org/10.1017/S1755020319000352

R. Ishigaki, K. Kikuchi, Tree-Sequent Methods for Subintuitionistic Predicate Logics, [in:] N. Olivetti (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 4548 of Lecture Notes in Computer Science, Springer, Berlin-Heidelberg (2007), pp. 149–164. DOI: https://doi.org/10.1007/978-3-540-73099-6_13

S. Kanger, Provability in logic, Almqvist & Wiksell (1957).

R. Kashima, Cut-free sequent calculi for some tense logics, Studia Logica, vol. 53(1) (1994), pp. 119–135, DOI: https://doi.org/10.1007/978-3-319-10061-6_4 DOI: https://doi.org/10.1007/BF01053026

M. Kracht, Power and Weakness of the Modal Display Calculus, [in:] H. Wansing (ed.), Proof Theory of Modal Logic, Springer Netherlands, Dordrecht (1996), pp. 93–121, DOI: https://doi.org/10.1007/978-94-017-2798-3_7 DOI: https://doi.org/10.1007/978-94-017-2798-3_7

S. A. Kripke, Semantical Analysis of Intuitionistic Logic I, [in:] J. Crossley, M. Dummett (eds.), Formal Systems and Recursive Functions, vol. 40 of Studies in Logic and the Foundations of Mathematics, Elsevier (1965), pp. 92–130, DOI: https://doi.org/10.1016/S0049-237X(08)71685-9 DOI: https://doi.org/10.1016/S0049-237X(08)71685-9

H. Kurokawa, Hypersequent Calculi for Modal Logics Extending S4, New Frontiers in Artificial Intelligence, (2013), pp. 51–68. DOI: https://doi.org/10.1007/978-3-319-10061-6_4

H. Kushida, M. Okada, A proof-theoretic study of the correspondence of classical logic and modal logic, Journal of Symbolic Logic, vol. 68(4) (2003), pp. 1403–1414, DOI: https://doi.org/10.2178/jsl/1067620195 DOI: https://doi.org/10.2178/jsl/1067620195

R. Kuznets, Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi, [in:] L. Michael, A. Kakas (eds.), Logics in Artificial Intelligence, vol. 10021 of Lecture Notes in Computer Science, Springer International Publishing, Cham (2016), pp. 320–335, DOI: https://doi.org/10.1007/978-3-319-48758-8_21 DOI: https://doi.org/10.1007/978-3-319-48758-8_21

R. Kuznets, B. Lellmann, Interpolation for Intermediate Logics via Hyper- and Linear Nested Sequents, [in:] G. Bezhanishvili, G. D’Agostino, G. Metcalfe, T. Studer (eds.), Advances in Modal Logic 12, College Publications (2018), pp. 473–492, URL: http://www.aiml.net/volumes/volume12/Kuznets-Lellmann.pdf

O. Lahav, From Frame Properties to Hypersequent Rules in Modal Logics, [in:] 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25–28, 2013(2013), pp. 408–417, DOI: https://doi.org/10.1109/LICS.2013.47 DOI: https://doi.org/10.1109/LICS.2013.47

D. Leivant, Proof theoretic methodology for propositional dynamic logic, [in:] J. Díaz, I. Ramos (eds.), Formalization of Programming Concepts, Springer, Berlin-Heidelberg (1981), pp. 356–373, DOI: https://doi.org/10.1007/3-540-10699-5_111 DOI: https://doi.org/10.1007/3-540-10699-5_111

B. Lellmann, Linear Nested Sequents, 2-Sequents and Hypersequents, [in:] H. De Nivelle (ed.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 9323 of Lecture Notes in Computer Science, Springer International Publishing, Cham (2015), pp. 135–150, DOI: https://doi.org/10.1007/978-3-319-24312-2_10 DOI: https://doi.org/10.1007/978-3-319-24312-2_10

B. Lellmann, Hypersequent rules with restricted contexts for propositional modal logics, Theoretical Computer Science, vol. 656 (2016), pp. 76–105, DOI: https://doi.org/https://doi.org/10.1016/j.tcs.2016.10.004 DOI: https://doi.org/10.1016/j.tcs.2016.10.004

B. Lellmann, D. Pattinson, Correspondence between modal Hilbert axioms and sequent rules with an application to S5, [in:] Automated Reasoning with Analytic Tableaux and Related Methods: 22nd International Conference, TABLEAUX 2013, Nancy, France, September 16–19, 2013, Springer (2013), pp. 219–233, DOI: https://doi.org/10.1007/978-3-642-40537-2_19 DOI: https://doi.org/10.1007/978-3-642-40537-2_19

B. Lellmann, E. Pimentel, Proof Search in Nested Sequent Calculi, [in:] M. Davis, A. Fehnker, A. McIver, A. Voronkov (eds.), Logic for Programming, Artificial Intelligence, and Reasoning – 20th International Conference, LPAR-20, vol. 9450 of Lecture Notes in Computer Science, Springer-Verlag, Berlin-Heidelberg (2015), p. 558–574, DOI: https://doi.org/10.1007/978-3-662-48899-7_39 DOI: https://doi.org/10.1007/978-3-662-48899-7_39

I. Lewis, A survey of symbolic logic, University of California Press (1918). DOI: https://doi.org/10.1525/9780520398252

D. Lewis, Counterfactuals, Blackwell, Hobokin (1973).

T. S. Lyon, On the Correspondence between Nested Calculi and Semantic Systems for Intuitionistic Logics, Journal of Logic and Computation, vol. 31(1) (2020), pp. 213–265, DOI: https://doi.org/10.1093/logcom/exaa078 DOI: https://doi.org/10.1093/logcom/exaa078

T. S. Lyon, Syntactic Cut-Elimination for Intuitionistic Fuzzy Logic via Linear Nested Sequents, [in:] S. N. Artëmov, A. Nerode (eds.), Logical Foundations of Computer Science – International Symposium, LFCS 2020, Deerfield Beach, FL, USA, January 4–7, 2020, vol. 11972 of Lecture Notes in Computer Science, Springer (2020), pp. 156–176, DOI: https://doi.org/10.1007/978-3-030-36755-8_11 DOI: https://doi.org/10.1007/978-3-030-36755-8_11

T. S. Lyon, Nested Sequents for Intuitionistic Modal Logics via Structural Refinement, [in:] A. Das, S. Negri (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer International Publishing, Cham (2021), pp. 409–427, DOI: https://doi.org/https://doi.org/10.1007/978-3-030-86059-2_24 DOI: https://doi.org/10.1007/978-3-030-86059-2_24

T. S. Lyon, Refining Labelled Systems for Modal and Constructive Logics with Applications, Ph.D. thesis, Technische Universität Wien (2021).

T. S. Lyon, Nested Sequents for Intermediate Logics: The Case of Gödel-Dummett Logics, Journal of Applied Non-Classical Logics, vol. 33(2) (2023), pp. 121–164, DOI: https://doi.org/10.1080/11663081.2023.2233346 DOI: https://doi.org/10.1080/11663081.2023.2233346

T. S. Lyon, Realizing the Maximal Analytic Display Fragment of Labeled Sequent Calculi for Tense Logics, Found on arXiv, (2024), URL: https://arxiv.org/abs/2406.19882

T. S. Lyon, Unifying Sequent Systems for Gödel-Löb Provability Logic via Syntactic Transformations, [in:] J. Endrullis, S. Schmitz (eds.),33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), vol. 326 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2025), pp. 42:1–42:23, DOI: https://doi.org/10.4230/LIPIcs.CSL.2025.42

T. S. Lyon, L. Gómez Álvarez, Automating Reasoning with Standpoint Logic via Nested Sequents, [in:] Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning (2022), pp. 257–266, DOI: https://doi.org/10.24963/kr.2022/26 DOI: https://doi.org/10.24963/kr.2022/26

T. S. Lyon, E. Orlandelli, Nested Sequents for Quantified Modal Logics, [in:] R. Ramanayake, J. Urban (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, Springer Nature Switzerland, Cham (2023), pp. 449–467, DOI: https://doi.org/10.1007/978-3-031-43513-3_24 DOI: https://doi.org/10.1007/978-3-031-43513-3_24

T. S. Lyon, P. Ostropolski-Nalewaja, Foundations for an Abstract Proof Theory in the Context of Horn Rules, Found on arXiv, (2024), URL: https://arxiv.org/abs/2304.05697

T. S. Lyon, I. Shillito, A. Tiu, Taking Bi-Intuitionistic Logic First-Order: A Proof-Theoretic Investigation via Polytree Sequents, [in:] J. Endrullis, S. Schmitz (eds.), 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025), vol. 326 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2025), pp. 41:1–41:23, DOI: https://doi.org/10.4230/LIPIcs.CSL.2025.41

T. S. Lyon, A. Tiu, R. Goré, R. Clouston, Syntactic Interpolation for Tense Logics and Bi-Intuitionistic Logic via Nested Sequents, [in:] M. Fernández, A. Muscholl (eds.), 28th EACSL Annual Conference on Computer Science Logic, CSL 2020, vol. 152 of LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020), pp. 28:1–28:16, DOI: https://doi.org/10.4230/LIPIcs.CSL.2020.28

T. S. Lyon, K. van Berkel, Automating Agential Reasoning: Proof-Calculi and Syntactic Decidability for STIT Logics, [in:] M. Baldoni, M. Dastani, B. Liao, Y. Sakurai, R. Zalila Wenkstern (eds.), PRIMA 2019: Principles and Practice of Multi-Agent Systems - 22nd International Conference, vol. 11873 of Lecture Notes in Computer Science, Springer International Publishing, Cham (2019), pp. 202–218. DOI: https://doi.org/10.1007/978-3-030-33792-6_13

T. S. Lyon, K. van Berkel, Proof Theory and Decision Procedures for Deontic STIT Logics, Journal of Artificial Intelligence Research, vol. 81 (2024), pp. 837–876, DOI: https://doi.org/https://doi.org/10.48550/arXiv.2402.03148 DOI: https://doi.org/10.1613/jair.1.15710

S. Maehara, Eine Darstellung der Intuitionistischen Logik in der Klassischen, Nagoya Mathematical Journal, vol. 7 (1954), p. 45–64, DOI: https://doi.org/10.1017/S0027763000018055 DOI: https://doi.org/10.1017/S0027763000018055

S. Maehara, On the interpolation theorem of Craig, Sûgaku, vol. 12(4) (1960), pp. 235–237.

S. Marin, M. Morales, L. Straßburger, A fully labelled proof system for intuitionistic modal logics, Journal of Logic and Computation, vol. 31(3) (2021), pp. 998–1022, DOI: https://doi.org/10.1093/logcom/exab020 DOI: https://doi.org/10.1093/logcom/exab020

A. Masini, 2-sequent calculus: A proof theory of modalities, Annals of Pure and Applied Logic, vol. 58(3) (1992), pp. 229–246, DOI: https://doi.org/10.1016/0168-0072(92)90029-Y DOI: https://doi.org/10.1016/0168-0072(92)90029-Y

A. Masini, 2-sequent calculus: Intuitionism and natural deduction, Journal of Logic and Computation, vol. 3(5) (1993), pp. 533–562, DOI: https://doi.org/10.1093/logcom/3.5.533 DOI: https://doi.org/10.1093/logcom/3.5.533

L. McMillan, Interpolation and Model Checking, [in:] E. M. Clarke, T. A. Henzinger, H. Veith, R. Bloem (eds.), Handbook of Model Checking, Springer International Publishing, Cham (2018), pp. 421–446, DOI: https://doi.org/10.1007/978-3-319-10575-8_14 DOI: https://doi.org/10.1007/978-3-319-10575-8_14

G. Metcalfe, N. Olivetti, D. M. Gabbay, Sequent and hypersequent calculi for abelian and Łukasiewicz logics, ACM Transactions on Computational Logic, vol. 6(3) (2005), pp. 578–613, DOI: https://doi.org/10.1145/1071596.1071600 DOI: https://doi.org/10.1145/1071596.1071600

E. Mints, Some calculi of modal logic, Trudy Matematicheskogo Instituta imeni VA Steklova, vol. 98 (1968), pp. 88–111.

E. Mints, Studies in constructive mathematics and mathematical logic. Part V, Nauka, Leningrad. Otdel, chap. Cut-elimination theorem for relevant logics (in Russian) (1972), pp. 90–97.

G. E. Mints, Indexed systems of sequents and cut-elimination, Journal of Philosophical Logic, vol. 26(6) (1997), pp. 671–696, DOI: https://doi.org/10.1023/A:1017948105274 DOI: https://doi.org/10.1023/A:1017948105274

S. Negri, Proof analysis in modal logic, Journal of Philosophical Logic, vol. 34(5–6) (2005), p. 507, DOI: https://doi.org/10.1007/s10992-005-2267-3 DOI: https://doi.org/10.1007/s10992-005-2267-3

P. W. O’Hearn, D. Pym, The Logic of Bunched Implications, Bulletin of Symbolic Logic, vol. 5(2) (1999), pp. 215–244, DOI: https://doi.org/https://doi.org/10.2307/421090 DOI: https://doi.org/10.2307/421090

E. Pimentel, R. Ramanayake, B. Lellmann, Sequentialising Nested Systems, [in:] S. Cerrito, A. Popescu (eds.), Automated Reasoning with Analytic Tableaux and Related Methods, vol. 11714 of Lecture Notes in Computer Science, Springer International Publishing, Cham (2019), pp. 147–165, DOI: https://doi.org/10.1007/978-3-030-29026-9_9 DOI: https://doi.org/10.1007/978-3-030-29026-9_9

F. Poggiolesi, A Cut-free Simple Sequent calculus for Modal Logic S5,The Review of Symbolic Logic, vol. 1(1) (2008), p. 3–15, DOI: https://doi.org/10.1017/S1755020308080040 DOI: https://doi.org/10.1017/S1755020308080040

F. Poggiolesi, The Method of Tree-Hypersequents for Modal Propositional Logic, [in:] D. Makinson, J. Malinowski, H. Wansing (eds.), Towards Mathematical Philosophy, vol. 28 of Trends in logic, Springer (2009), pp. 31–51, DOI: https://doi.org/10.1007/978-1-4020-9084-4_3 DOI: https://doi.org/10.1007/978-1-4020-9084-4_3

F. Poggiolesi, A Tree-Hypersequent Calculus for the Modal Logic of Provability, Springer Netherlands, Dordrecht (2011), pp. 187–201, DOI: https://doi.org/10.1007/978-90-481-9670-8_10 DOI: https://doi.org/10.1007/978-90-481-9670-8_10

F. Poggiolesi, G. Restall, Interpreting and Applying Proof Theories for Modal Logic, Palgrave Macmillan UK, London (2012), pp. 39–62, DOI: https://doi.org/10.1057/9781137003720_4 DOI: https://doi.org/10.1057/9781137003720_4

E. Pottinger, Uniform, cut-free formulations of T, S4 and S5, Journal of Symbolic Logic, vol. 48(3) (1983), p. 900.

N. Prior, Time and Modality, Oxford University Press (1957).

D. Pym, The Semantics and Proof Theory of the Logic of Bunched Implications, vol. 26 of Applied Logic Series, Kluwer Academic Publishers (2002), DOI: https://doi.org/10.1007/978-94-017-0091-7 DOI: https://doi.org/10.1007/978-94-017-0091-7

S. Read, Semantic Pollution and Syntactic Purity, The Review of Symbolic Logic, vol. 8(4) (2015), DOI: https://doi.org/10.1017/S1755020315000210 DOI: https://doi.org/10.1017/S1755020315000210

G. Restall, Proofnets for S5: sequents and circuits for modal logic, [in:]Logic Colloquium 2005, Lecture Notes in Logic, vol. 28, Cambridge University Press (2007), pp. 151–172. DOI: https://doi.org/10.1017/CBO9780511546464.012

K. Simpson, The proof theory and semantics of intuitionistic modal logic, Ph.D. thesis, University of Edinburgh. College of Science and Engineering. School of Informatics (1994).

K. Slaney, Minlog: A Minimal Logic Theorem Prover, [in:] W. McCune (ed.), Automated Deduction – CADE-14, 14th International Conference on Automated Deduction, Townsville, North Queensland, Australia, vol. 1249 of Lecture Notes in Computer Science, Springer (1997), pp. 268–271, DOI: https://doi.org/10.1007/3-540-63104-6_27 DOI: https://doi.org/10.1007/3-540-63104-6_27

L. Straßburger, Cut Elimination in Nested Sequents for Intuitionistic Modal Logics, [in:] F. Pfenning (ed.), Foundations of Software Science and Computation Structures, vol. 7794 of Lecture Notes in Computer Science, Springer, Berlin-Heidelberg (2013), pp. 209–224, DOI: https://doi.org/10.1007/978-3-642-37075-5_14 DOI: https://doi.org/10.1007/978-3-642-37075-5_14

A. Tiu, E. Ianovski, R. Goré, Grammar Logics in Nested Sequent Calculus: Proof Theory and Decision Procedures, [in:] T. Bolander, T. Braüner, S. Ghilardi, L. S. Moss (eds.), Advances in Modal Logic 9, College Publications (2012), pp. 516–537, URL: http://www.aiml.net/volumes/volume9/Tiu-Ianovski-Gore.pdf

K. van Berkel, T. S. Lyon, Cut-Free Calculi and Relational Semantics for Temporal STIT Logics, [in:] F. Calimeri, N. Leone, M. Manna (eds.), Logics in Artificial Intelligence, Springer International Publishing, Cham (2019), pp. 803–819, DOI: https://doi.org/10.1007/978-3-030-19570-0_52 DOI: https://doi.org/10.1007/978-3-030-19570-0_52

K. van Berkel, T. S. Lyon, The Varieties of Ought-implies-Can and Deontic STIT Logic, [in:] F. Liu, A. Marra, P. Portner, F. V. D. Putte (eds.), Deontic Logic and Normative Systems: 15th International Conference (DEON2020/2021), College Publications (2021), URL: https://www.collegepublications.co.uk/DEON/Van%20Berkel%20&%20Lyon_DEON2020.pdf

L. Viganò, Labelled Non-Classical Logics, Springer Science & Business Media (2000), DOI: https://doi.org/10.1007/978-1-4757-3208-5 DOI: https://doi.org/10.1007/978-1-4757-3208-5

H. Wansing, Sequent calculi for normal modal propositional logics, Journal of Logic and Computation, vol. 4(2) (1994), pp. 125–142, DOI: https://doi.org/10.1093/logcom/4.2.125 DOI: https://doi.org/10.1093/logcom/4.2.125

H. Wansing, Sequent Systems for Modal Logics, [in:] D. M. Gabbay, F. Guenthner (eds.), Handbook of Philosophical Logic: Volume 8, Springer Netherlands, Dordrecht (2002), pp. 61–145, DOI: https://doi.org/10.1007/978-94-010-0387-2_2 DOI: https://doi.org/10.1007/978-94-010-0387-2_2

F. Wolter, On Logics with Coimplication, Journal of Philosophical Logic, vol. 27(4) (1998), pp. 353–387, DOI: https://doi.org/10.1023/A:1004218110879 DOI: https://doi.org/10.1023/A:1004218110879