P. Abate, R. Goré, and F. Widmann, Cut-free singlepass tableaux for the logic of common knowledge, Workshop on Agents and Deduction at TABLEAUX'07, 2007.

C. Areces, P. Fontaine, and S. Merz, Modal satisfiability via SMT solving, Software, Services, and Systems -Essays Dedicated to Martin Wirsing, pp.30-45, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01127966

G. Audemard and L. Simon, Predicting learnt clauses quality in modern SAT solvers, Proc. of IJCAI'09, pp.399-404, 2009.

P. Balsiger, A. Heuerding, and S. Schwendimann, A Benchmark Method for the Propositional Modal Logics K, KT, S4, J. Autom. Reasoning, vol.24, issue.3, pp.297-317, 2000.

M. Bienvenu, H. Fargier, and P. Marquis, Knowledge compilation in the modal logic S5, Proc. of AAAI'10, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00624482

R. E. Bryant, Graph-based algorithms for boolean function manipulation, IEEE Trans. Computers, vol.35, issue.8, pp.677-691, 1986.

R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi, Reasoning About Knowledge, 1995.

M. Fairtlough and M. Mendler, An Intuitionistic Modal Logic with Applications to the Formal Verification of Hardware, Proc. of CSL'94, pp.354-368, 1994.

M. Fitting, Modality and databases, Proc. of TABLEAUX'00, pp.19-39, 2000.

O. Gasquet, A. Herzig, D. Longin, and M. Sahade, LoTREC: Logical Tableaux Research Engineering Companion, Proc. of TABLEAUX'05, pp.318-322, 2005.

F. Giunchiglia and R. Sebastiani, Building Decision Procedures for Modal Logics from Propositional Decision Procedures: The Case Study of Modal K(m), Inf. Comput, vol.162, issue.1-2, pp.158-178, 2000.

E. Giunchiglia and A. Tacchella, System description: *SAT: A platform for the development of modal decision procedures, Proc. of CADE'00, pp.291-296, 2000.

E. Giunchiglia and A. Tacchella, A subset-matching size-bounded cache for testing satisfiability in modal logics, Ann. Math. Artif. Intell, vol.33, issue.1, pp.39-67, 2001.

E. Giunchiglia, R. Sebastiani, F. Giunchiglia, and A. Tacchella, SAT vs. Translation based decision procedures for modal logics: a comparative evaluation, Journal of Applied Non-Classical Logics, vol.10, issue.2, pp.145-172, 2000.

E. Giunchiglia, F. Giunchiglia, and A. Tacchella, The sat-based approach for classical modal logics, Proc. of AI*IA'99, pp.95-106, 1999.

E. Giunchiglia, A. Tacchella, and F. Giunchiglia, SAT-Based Decision Procedures for Classical Modal Logics, J. Autom. Reasoning, vol.28, issue.2, pp.143-171, 2002.

D. Götzmann, M. Kaminski, and G. Smolka, Spartacus: A tableau prover for hybrid logic, Electr. Notes Theor. Comput. Sci, vol.262, pp.127-139, 2010.

A. Haken, The intractability of resolution, Theoretical Computer Science, vol.39, issue.0, pp.297-308, 1985.

J. Y. Halpern and L. C. Rêgo, Characterizing the NP-PSPACE Gap in the Satisfiability Problem for Modal Logic, Proc. of IJCAI'07, pp.2306-2311, 2007.

G. Hoffmann, . Nancy, M. Kaminski, and T. Tebbi, InKreSAT: Modal Reasoning via Incremental Reduction to SAT, Proc. of CADE'13, pp.436-442, 2010.

R. E. Ladner, The Computational Complexity of Provability in Systems of Modal Propositional Logic, SIAM J. Comput, vol.6, issue.3, pp.467-480, 1977.

E. Lorini and F. Schwarzentruber, A modal logic of epistemic games, Games, vol.1, issue.4, pp.478-526, 2010.

F. Massacci and F. M. Donini, Design and results of TANCS-2000 non-classical (modal) systems comparison, Proc. of Tableaux'00, pp.52-56, 2000.

F. Massacci, Design and results of the tableaux-99 non-classical (modal) systems comparison, Proc. of Tableaux'99, pp.14-18, 1999.

F. Masssacci, Single step tableaux for modal logics: Methodology, computations, algorithms, Journal of Autom, vol.24, issue.3, pp.319-364, 2000.

A. Niveau and B. Zanuttini, Efficient Representations for the Modal Logic S5, Proc. of IJCAI'16, pp.1223-1229, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01311642

P. F. Patel-schneider and R. Sebastiani, A new general method to generate random modal formulae for testing decision procedures, J. Artif. Intell. Res, vol.18, pp.351-389, 2003.

P. Blackburn, J. V. Wolter, and F. , Handbook of Modal Logic, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00580143

J. A. Robinson and A. Voronkov, Handbook of Automated Reasoning (in 2 volumes), 2001.

R. Sebastiani and A. Tacchella, SAT Techniques for Modal and Description Logics, Handbook of Satisfiability, vol.185, pp.781-824, 2009.

R. Sebastiani and M. Vescovi, Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability, JAIR, vol.35, issue.1, p.343, 2009.

R. Sebastiani and A. Villafiorita, Sat-based decision procedures for normal modal logics: A theoretical framework, Proc. of AIMSA'98, pp.377-388, 1998.

D. Tishkovsky, R. A. Schmidt, and M. Khodadadi, The Tableau Prover Generator MetTeL2, Proc. of JELIA'12, pp.492-495, 2012.

G. S. Tseitin, On the Complexity of Derivation in Propositional Calculus, pp.466-483, 1983.

T. M. Vii, K. Crary, and R. Harper, Distributed control flow with classical modal logic, Proc. of CSL'05, pp.51-69, 2005.

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., SPASS version 3.5, Proc. of CADE'09, pp.140-145, 2009.