R. Arisaka, A. Das, and L. Straßburger, On nested sequents for constructive modal logics, Logical Methods in Computer Science, vol.11, issue.3, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01093143

,

B. Beckert and J. Posegga, leantap: Lean tableau-based deduction, Journal of Automated Reasoning, vol.15, issue.3, pp.339-358, 1995.

K. Brünnler, Deep sequent systems for modal logic, Archive for Mathematical Logic, vol.48, issue.6, pp.551-577, 2009.

L. Catach, Tableaux: A general theorem prover for modal logics, Journal of automated reasoning, vol.7, issue.4, pp.489-510, 1991.

K. Chaudhuri, S. Marin, and L. Straßburger, Focused and synthetic nested sequents, Proceedings of the 19th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2016.
URL : https://hal.archives-ouvertes.fr/hal-01417618

K. Chaudhuri, S. Marin, and L. Straßburger, Modular focused proof systems for intuitionistic modal logics, 1st International Conference on Formal Structures for Computation and Deduction, FSCD 2016, vol.52, pp.1-16, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01417603

G. Fischer-servi, Axiomatizations for some intuitionistic modal logics, Rend. Sem. Mat. Univers. Politecn. Torino, vol.42, issue.3, pp.179-194, 1984.

D. Galmiche and Y. Salhi, Label-free proof systems for intuitionistic modal logic IS5, International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp.255-271, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00580298

G. Gentzen, Untersuchungenüber das logische Schließen. I, Mathematische Zeitschrift, vol.39, pp.176-210, 1935.

R. Goré, L. Postniece, and A. Tiu, Cut-elimination and proof search for biintuitionistic tense logic, Advances in Modal Logic, pp.156-177, 2010.

R. Kashima, Cut-free sequent calculi for some tense logics, Studia Logica, vol.53, issue.1, pp.119-136, 1994.

R. Kuznets and L. Straßburger, Maehara-style modal nested calculi, Archive for Mathematical Logic, vol.58, issue.3-4, pp.359-385, 2019.
URL : https://hal.archives-ouvertes.fr/hal-01644750

B. Lellmann, Combining monotone and normal modal logic in nested sequentswith countermodels, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pp.203-220, 2019.

B. Lellmann and E. Pimentel, Modularisation of sequent calculi for normal and nonnormal modalities, ACM Transactions on Computational Logic (TOCL), vol.20, issue.2, p.7, 2019.

S. Maehara, Eine darstellung der intuitionistischen logik in der klassischen, Nagoya mathematical journal, vol.7, pp.45-64, 1954.

S. Marin, Modal proof theory through a focused telescope, 2018.
URL : https://hal.archives-ouvertes.fr/tel-01951291

S. Marin and L. Straßburger, Label-free Modular Systems for Classical and Intuitionistic Modal Logics, Advances in Modal Logic 10, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01092148

N. Olivetti and G. L. Pozzato, Nescond: an implementation of nested sequent calculi for conditional logics, International Joint Conference on Automated Reasoning, pp.511-518, 2014.

J. Otten, How to build an automated theorem prover, 2019.

G. D. Plotkin and C. P. Stirling, A framework for intuitionistic modal logic, Theoretical Aspects of Reasoning About Knowledge, 1986.

F. Poggiolesi, The method of tree-hypersequents for modal propositional logic, Trends in Logic, vol.28, pp.31-51, 2009.
URL : https://hal.archives-ouvertes.fr/halshs-00775815

A. Simpson, The Proof Theory and Semantics of Intuitionistic Modal Logic, 1994.

L. Straßburger, Cut elimination in nested sequents for intuitionistic modal logics, FoSSaCS'13, vol.7794, pp.209-224, 2013.