C. Areces, P. Fontaine, and S. Merz, Modal Satisfiability via SMT Solving. Dans Software, Services, and Systems, pp.30-45, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01127966

G. Audemard, J. Lagniez, and L. Simon, Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction, Proc. of SAT'13, pp.309-317, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00845496

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

A. Biere and M. Heule, Hans van Maaren et Toby Walsh (rédacteurs): Handbook of Satisfiability, tome 185 de Frontiers in Artificial Intelligence and Applications, pp.978-979, 2009.

P. Blackburn, J. Van-benthem, and F. Wolter, Handbook of Modal Logic, tome 3, pp.978-0444516909, 2006.

B. F. Chellas, Modal Logic: An Introduction

E. M. Clarke, S. Orna-grumberg, Y. Jha, H. Lu, and . Veith, CounterExample-Guided Abstraction Refinement For Symbolic Model Checking, J. of the ACM, vol.50, issue.5, pp.752-794, 2003.

N. Eén and N. Sörensson, An Extensible SAT-solver

, Dans Proc. of SAT'03, pp.502-518, 2003.

D. M. Gabbay, A General Filtration Method For Modal Logics, Journal of Philosophical Logic, vol.1, issue.1, pp.29-34, 1972.

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

R. Goré, K. Olesen, and J. Thomson, Implementing Tableau Calculi Using BDDs: BDDTab System Description, Proc. of IJCAR'14, pp.337-343, 2014.

D. Götzmann, M. Kaminski, and G. Smolka, Spartacus: A Tableau Prover for Hybrid Logic. ENTCS, vol.262, pp.127-139, 2010.

I. Horrocks, U. Hustadt, U. Sattler, and R. A. Schmidt, Computational Modal Logic. Studies in Logic and Practical Reasoning, vol.3, pp.181-245, 2007.

M. Janota, W. Klieber, J. Marquessilva, and E. M. Clarke, Solving QBF with CounterExample Guided Refinement, Art. Int, vol.234, pp.1-25, 2016.

J. Lagniez, D. L. Berre, T. Lima, and V. Montmirail,

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

L. Kovács and A. Voronkov, First-Order Theorem Proving and Vampire, Proc. of CAV'13, pp.1-35, 2013.

S. Kripke, A Completeness Theorem in Modal Logic, J. Symb. Log, vol.24, issue.1, pp.1-14, 1959.

J. Lagniez, D. L. Marie, and . Berre, Tiago de Lima et Valentin Montmirail: A Recursive Shortcut for CE-GAR: Application To The Modal Logic K Satisfiability Problem, Proc. of IJCAI'17, 2017.

J. Lagniez, D. L. Marie, and . Berre, Tiago de Lima et Valentin Montmirail: A SAT-Based Approach For PSPACE Modal Logics, Proc. of KR'18, pp.651-652, 2018.

J. Lagniez and . Marquis, An Improved Decision-DNNF Compiler, Proc. of IJCAI'17, pp.667-673, 2017.

T. Matsuhisa, Core Equivalence in Economy for Modal Logic, Proc. of ICCS'03, Part II, pp.74-83, 2003.

C. Nalon, U. Hustadt, C. Dixon, and :. , A Resolution-Based Prover for Multimodal K, Proc. of IJCAR'16, pp.406-415, 2016.

U. Oztok and A. Darwiche, On Compiling CNF into Decision-DNNF, Proc. of CP'14, pp.42-57, 2014.

S. Prestwich, :. David, ;. Cnf-encodings, and A. Biere, , vol.4, pp.75-97

J. Rintanen, S. Planning, and A. Dans-biere, , vol.4, pp.483-504

J. A. Robinson and A. Voronkov, rédac-teurs): Handbook of Automated Reasoning, tome 1, 2001.

H. Sahlqvist, Completeness and correspondence in the first and second order semantics for modal logic, Proc. of the 3rd Scandinavian Logic Sumposium, 1973.

H. Samulowitz and F. Bacchus, Using SAT in QBF, Proc. of CP'05, pp.578-592, 2005.

T. Sang, F. Bacchus, P. Beame, and A. Henry, Kautz et Toniann Pitassi: Combining Component Caching and Clause Learning for E?ective Model Counting, Proc. of SAT'04, 2004.

R. Sebastiani and D. Mcallester, New Upper Bounds for Satisfiability in Modal Logics the Casestudy of Modal K, 1997.

R. Sebastiani, A. Tacchella, ;. Biere, and A. , SAT Techniques for Modal and Description Logics, vol.4, pp.978-979

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, pp.343-389, 2009.

. Thurley, Marc: sharpSAT -Counting Models with Advanced Component Caching and Implicit BCP, Proc. of SAT'06, pp.424-429, 2006.

J. P. Toriz and . Munoz, Iván Martínez Ruiz et José Ramón Enrique Arrazola-Ramírez: On Automatic Theorem Proving with ML, Proc. of MI-CAI'14, pp.231-236, 2014.

D. Tsarkov and I. Horrocks, FaCT++ Description Logic Reasoner: System Description, Proc. of IJCAR'06, pp.292-297, 2006.

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

V. Benthem and J. , Modal Logic For Open Minds, tome 1. Center for the Study of Language and Inf, pp.978-1575865980, 2010.