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 https://orcid.org/0000-0003-3214-0828
Agata Ciabattoni Vienna University of Technology, Austria https://orcid.org/0000-0001-6947-8772
Didier Galmiche Université de Lorraine, CNRS, LORIA, France https://orcid.org/0000-0002-9968-5323
Marianna Girlando University of Amsterdam, Netherlands https://orcid.org/0000-0002-9384-1356
Dominique Larchey-Wendling Université de Lorraine, CNRS, LORIA, France https://orcid.org/0000-0001-9860-7203
Daniel Méry Université de Lorraine, CNRS, LORIA, France https://orcid.org/0000-0002-1886-2106
Nicola Olivetti Aix-Marseille University, France https://orcid.org/0000-0001-6254-3754
Revantha Ramanayake University of Groningen, Netherlands 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
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1017/CBO9781107050884

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

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar

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
Google Scholar DOI: https://doi.org/10.2307/2275431

R. Dyckhoff, Intuitionistic decision procedures since Gentzen, Advances in Proof Theory, (2016), pp. 245–267.
Google Scholar 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
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar

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
Google Scholar 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
Google Scholar

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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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).
Google Scholar

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

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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar DOI: https://doi.org/10.1007/978-3-540-73099-6_13

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

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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1007/978-3-662-48899-7_39

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

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

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
Google Scholar 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
Google Scholar 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
Google Scholar 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).
Google Scholar

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
Google Scholar 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
Google Scholar

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
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar

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
Google Scholar

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
Google Scholar

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.
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1017/S0027763000018055

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

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar

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.
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar 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.
Google Scholar

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

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
Google Scholar 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
Google Scholar 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.
Google Scholar 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).
Google Scholar

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
Google Scholar 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
Google Scholar 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
Google Scholar

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
Google Scholar 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
Google Scholar

L. Viganò, Labelled Non-Classical Logics, Springer Science & Business Media (2000), DOI: https://doi.org/10.1007/978-1-4757-3208-5
Google Scholar 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
Google Scholar 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
Google Scholar 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
Google Scholar DOI: https://doi.org/10.1023/A:1004218110879