H. Andréka, J. Van-benthem, and I. Németi, Modal Languages and Bounded Fragments of Predicate Logic, Journal of Philosophical Logic, vol.60, issue.5, pp.217-274, 1998.
DOI : 10.2307/2275853

. Areces, Logic Engineering. The Case of Description and Hybrid Logics, 2000.

C. Areces and D. Gorín, Resolution with Order and Selection for Hybrid Logics, Journal of Automated Reasoning, vol.22, issue.4, 2004.
DOI : 10.1007/3-540-52335-9_55

URL : https://hal.archives-ouvertes.fr/inria-00519035

C. Areces and B. Cate, Hybrid logics, pp.821-868, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00549320

C. Areces, P. Blackburn, and M. Marx, A Road-Map on Complexity for Hybrid Logics, Computer Science Logic, number 1683 in LNCS Proceedings of the 8th Annual Conference of the EACSL, pp.307-321, 1999.
DOI : 10.1007/3-540-48168-0_22

URL : https://hal.archives-ouvertes.fr/inria-00000337

C. Areces, R. Gennari, J. Heguiabere, and M. De-rijke, Tree-based heuristics in modal theorem proving, Proc. of ECAI'2000, pp.199-203, 2000.
URL : https://hal.archives-ouvertes.fr/inria-00000338

C. Areces, P. Blackburn, and M. Marx, Abstract, The Journal of Symbolic Logic, vol.XLI, issue.03, pp.977-1010, 2001.
DOI : 10.1093/jigpal/8.5.653

C. Areces, H. De-nivelle, and M. De-rijke, Resolution in Modal, Description and Hybrid Logic, Journal of Logic and Computation, vol.11, issue.5, pp.717-736, 2001.
DOI : 10.1093/logcom/11.5.717

URL : https://hal.archives-ouvertes.fr/inria-00000336

C. Areces, D. Figueira, S. Figueira, and S. Mera, Expressive Power and Decidability for Memory Logics, Logic, Language, Information and Computation, pp.56-68
DOI : 10.1007/978-3-540-69937-8_7

URL : https://hal.archives-ouvertes.fr/inria-00323834

Y. Auffray and P. Enjalbert, Modal Theorem Proving: An Equational Viewpoint, Proc. of the 11th International Joint Conference on Artificial Intelligence, pp.441-445, 1989.
DOI : 10.1093/logcom/2.3.247

Y. Auffray and P. Enjalbert, Modal Theorem Proving: An Equational Viewpoint, Journal of Logic and Computation, vol.2, issue.3, pp.247-295, 1992.
DOI : 10.1093/logcom/2.3.247

P. Auffray, J. Enjalbert, and . Hebrard, Strategies for modal resolution: Results and problems, Journal of Automated Reasoning, vol.4, issue.1, pp.1-38, 1990.
DOI : 10.1007/BF00302639

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

L. Bachmair and H. Ganzinger, Resolution Theorem Proving, pp.19-99, 2001.
DOI : 10.1016/B978-044450813-3/50004-7

L. Bachmair and H. Ganzinger, Rewrite-based Equational Theorem Proving with Selection and Simplification, Journal of Logic and Computation, vol.4, issue.3, pp.217-247, 1994.
DOI : 10.1093/logcom/4.3.217

H. Barendregt, The lambda calculus: its syntax and semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.

P. Blackburn, Internalizing labelled deduction, Journal of Logic and Computation, vol.10, issue.1, pp.137-168, 2000.
DOI : 10.1093/logcom/10.1.137

P. Blackburn and M. Marx, Tableaux for Quantified Hybrid Logic, Automated Reasoning with Analytic Tableaux and Related Method, number 2381 in LNAI, pp.38-52, 2002.
DOI : 10.1007/3-540-45616-3_4

URL : https://hal.archives-ouvertes.fr/inria-00100892

P. Blackburn and B. Cate, Pure Extensions, Proof Rules, and Hybrid Axiomatics, Studia Logica, vol.40, issue.3, pp.277-322, 2002.
DOI : 10.1111/j.1755-2567.1974.tb00077.x

URL : https://hal.archives-ouvertes.fr/inria-00119855

P. Blackburn, M. De-rijke, and Y. Venema, Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Sciene

P. Blackburn, F. Wolter, and J. Van-benthem, Handbook of Modal Logics, volume 3 of Studies in Logic and Practical Reasoning, 2006.

T. Bolander and P. Blackburn, Termination for Hybrid Tableaus, Journal of Logic and Computation, vol.17, issue.3, pp.517-554, 2007.
DOI : 10.1093/logcom/exm014

URL : http://www.imm.dtu.dk/~tb/BB06_rev.pdf

T. Bolander and P. Blackburn, Terminating Tableau Calculi for Hybrid Logics Extending K, Electronic Notes in Theoretical Computer Science, vol.231, issue.3, pp.21-39, 2009.
DOI : 10.1016/j.entcs.2009.02.027

URL : https://doi.org/10.1016/j.entcs.2009.02.027

T. Bolander and T. Brauner, Tableau-based Decision Procedures for Hybrid Logic, Journal of Logic and Computation, vol.16, issue.6, pp.737-763, 2006.
DOI : 10.1093/logcom/exl008

D. Brand, Proving Theorems with the Modification Method, SIAM Journal on Computing, vol.4, issue.4, pp.412-430, 1975.
DOI : 10.1137/0204036

T. Braüner, Natural Deduction for Hybrid Logic, Journal of Logic and Computation, vol.14, issue.3, pp.329-353, 2004.
DOI : 10.1093/logcom/14.3.329

T. Braüner, Two natural deduction systems for hybrid logic: A comparison, Journal of Logic, Language and Information, vol.13, issue.1, pp.1-23, 2004.
DOI : 10.1023/A:1026187215321

O. Clarke, D. Grumberg, and . Peled, Model checking, 1999.

H. De-nivelle and M. De-rijke, Deciding the guarded fragments by resolution, Journal of Symbolic Computation, vol.35, issue.1, pp.21-58, 2003.
DOI : 10.1016/S0747-7171(02)00092-5

H. De-nivelle and I. Pratt-hartmann, A Resolution-Based Decision Procedure for the Two-Variable Fragment with Equality, Proceedings of IJCAR 2001, pp.211-225, 2001.
DOI : 10.1007/3-540-45744-5_16

P. Enjalbert and L. Fariñas-del-cerro, Modal resolution in clausal form, Theoretical Computer Science, vol.65, issue.1, pp.1-33, 1989.
DOI : 10.1016/0304-3975(89)90137-0

L. Fariñas-del-cerro and A. Herzig, Linear modal deductions, Proc. of the 9th Conference on Automated Deduction, pp.487-499, 1988.
DOI : 10.1007/BFb0012851

J. Michael, R. E. Fischer, and . Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.11, pp.194-211, 1979.

M. Fitting, Destructive Modal Resolution, Journal of Logic and Computation, vol.1, issue.1, pp.83-97, 1990.
DOI : 10.1093/logcom/1.1.83

D. Gabbay, Expressive Functional Completeness in Tense Logic (Preliminary report), Aspects of Philosophical Logic, pp.91-117, 1981.
DOI : 10.1007/978-94-009-8384-7_4

H. Ganzinger and H. De-nivelle, A superposition decision procedure for the guarded fragment with equality, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.295-303, 1999.
DOI : 10.1109/LICS.1999.782624

M. Giese and W. Ahrendt, Hilbert???s ???-Terms in Automated Theorem Proving, Automated Reasoning with Analytic Tableaux and Related Methods, Intl. Conf. (TABLEAUX'99), volume 1617 of LNAI, pp.171-185, 1999.
DOI : 10.1007/3-540-48754-9_17

R. Goldblatt and S. Thomason, Axiomatic classes in propositional modal logic, Algebra and Logic, pp.163-173, 1975.
DOI : 10.1016/S0049-237X(08)70723-7

. Grädel, Why are modal logics so robustly decidable, Current Trends in Theoretical Computer Science. Entering the 21st Century, pp.393-408, 2001.

D. Harel, D. Kozen, and J. Tiuryn, Dynamic logic. Foundations of Computing, 2000.

M. Hennessy and R. Milner, Algebraic laws for nondeterminism and concurrency, Journal of the ACM, vol.32, issue.1, pp.137-161, 1985.
DOI : 10.1145/2455.2460

URL : https://www.scss.tcd.ie/Matthew.Hennessy/pubs/old/HMjacm85.pdf

J. Herbrand, Recherches sur la théorie de la démonstrations, Logical Writings. Reidel, 1930.

I. Horrocks, U. Hustadt, U. Sattler, and R. Schmidt, 4 Computational modal logic, pp.181-245, 2006.
DOI : 10.1016/S1570-2464(07)80007-3

URL : http://www.cs.man.ac.uk/~horrocks/Publications/download/2006/HHSS06.pdf

I. Horrocks and U. Sattler, A Tableau Decision Procedure for $\mathcal{SHOIQ}$, Journal of Automated Reasoning, vol.12, issue.2, pp.249-276, 2007.
DOI : 10.1016/j.websem.2007.03.004

U. Hustadt and R. A. Schmidt, An empirical analysis of modal theorem provers, Journal of Applied Non-Classical Logics, vol.18, issue.2, pp.479-522, 1999.
DOI : 10.1023/A:1005812220011

B. Jacobs and J. Rutten, A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, issue.33, pp.222-259, 1997.

W. Joyner and J. , Resolution Strategies as Decision Procedures, Journal of the ACM, vol.23, issue.3, pp.398-417
DOI : 10.1145/321958.321960

M. Kaminski and G. Smolka, Terminating Tableau Systems for Hybrid Logic with Difference and Converse, Journal of Logic, Language and Information, vol.9, issue.3, pp.437-464, 2003.
DOI : 10.1017/CBO9781107050884

URL : http://www.ps.uni-sb.de/Papers/abstracts/KSJoLLI2009.pdf

Y. Kazakov and B. Motik, A Resolution-Based Decision Procedure for $\mathcal{SHOIQ}$, Journal of Automated Reasoning, vol.40, issue.23 3, pp.89-116, 2008.
DOI : 10.1007/11814771_53

D. Knuth and P. Bendix, Simple Word Problems in Universal Algebras, Computational Algebra, pp.263-297, 1970.
DOI : 10.1007/978-3-642-81955-1_23

R. Ladner, The Computational Complexity of Provability in Systems of Modal Propositional Logic, SIAM Journal on Computing, vol.6, issue.3, pp.467-480, 1977.
DOI : 10.1137/0206033

A. Leisenring, Mathematical logic and Hilbert's -symbol, 1969.

C. Lewis, A Survey of Symbolic Logic Reprint of Chapters I?IV by, 1918.

E. Lusk, Controlling redundancy in large search spaces: Argonne-style theorem proving through the years, Proc. of the International Conference on Logic Programming and Automated Reasoning (LPAR'92), pp.96-106, 1992.
DOI : 10.1007/BFb0013052

W. Mccune and L. Wos, Experiments in automated deduction with condensed detachment, CADE-11: Proceedings of the 11th International Conference on Automated Deduction, pp.209-223, 1992.

. Meyer and . Applying, Applying 'design by contract', Computer, vol.25, issue.10, pp.40-51, 1992.
DOI : 10.1109/2.161279

G. Mints, Gentzen-type systems and resolution rules part I propositional logic, Proceedings of COLOG-88, pp.198-231, 1990.
DOI : 10.1007/3-540-52335-9_55

G. Mints, Resolution calculi for modal logics, Eight Papers Translated from the Russian, pp.1-14, 1989.
DOI : 10.1090/trans2/143/01

M. Mortimer, On languages with two variables, Mathematical Logic Quarterly, vol.27, issue.1, 1975.
DOI : 10.1002/malq.19750210118

M. Mundhenk, T. Schneider, T. Schwentick, and V. Weber, Complexity of hybrid logics over transitive frames, Proc. of Methods for Modalities of Informatik-Berichte, pp.62-78, 2003.
DOI : 10.1016/j.jal.2010.08.004

R. Nieuwenhuis and A. Rubio, Basic superposition is complete, Proc. of the 4th European Symposium on Programming, pp.371-389, 1992.
DOI : 10.1007/3-540-55253-7_22

R. Nieuwenhuis and A. Rubio, Paramodulation-Based Theorem Proving, pp.371-443, 2001.
DOI : 10.1016/B978-044450813-3/50009-6

URL : http://www-lsi.upc.es/~albert/papers/handbook.ps.gz

A. Nonnengart and C. Weidenbach, Computing Small Clause Normal Forms, pp.335-367, 2001.
DOI : 10.1016/B978-044450813-3/50008-4

H. Ohlbach, A resolution calculus for modal logics, Proc. of the 9th Conference on Automated Deduction, pp.500-516, 1988.
DOI : 10.1007/BFb0012852

H. Ohlbach, A resolution calculus for modal logics, 1988.
DOI : 10.1007/BFb0012852

URL : http://www.dcs.kcl.ac.uk/staff/ohlbach/homepage/publications/conferences/modal_resolution_cade.ps.gz

H. Ohlbach and R. Schmidt, Functional translation and second-order frame properties of modal logics, Journal of Logic and Computation, vol.7, issue.5, pp.581-603
DOI : 10.1093/logcom/7.5.581

H. Ohlbach, A. Nonnegart, M. De-rijke, and D. Gabbay, Encoding twovalued non-classical logics in classical logic, pp.1403-1486, 2001.
DOI : 10.1016/b978-044450813-3/50023-0

V. R. Pratt, Models of program logics, 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pp.115-122, 1979.
DOI : 10.1109/SFCS.1979.24

P. Rabe, G. Pudlák, W. Sutcliffe, and . Shen, Solving the $100 modal logic challenge, Journal of Applied Logic, vol.7, issue.1, pp.113-130, 2009.
DOI : 10.1016/j.jal.2007.07.007

URL : https://doi.org/10.1016/j.jal.2007.07.007

G. Robinson and L. Wos, Paramodulation and theorem-proving in firstorder, Machine Intelligence, vol.4, issue.21, pp.135-150, 1969.
DOI : 10.1142/9789812813411_0008

J. Robinson, A Machine-Oriented Logic Based on the Resolution Principle, Journal of the ACM, vol.12, issue.1, pp.23-41, 1965.
DOI : 10.1145/321250.321253

J. Rosser, Logic for mathematicians, 1953.

. Sangiorgi, On the origins of bisimulation and coinduction, ACM Transactions on Programming Languages and Systems, vol.31, issue.4, 2002.

. Schmidt, Decidability by resolution for propositional modal logics, Journal of Automated Reasoning, vol.22, issue.4, pp.379-396, 1999.
DOI : 10.1023/A:1006043519663

. Scott, A decision method for validity of sentences in two variables, Contribution to the " Twenty- Eighth Annual Meeting of the Association for Symbolic Logic, p.477, 1962.

R. Sebastiani and M. Vescovi, Automated reasoning in modal and description logics via SAT encoding: the case study of K m /ALC-satisfiability, Journal of Artificial Intelligence Research, vol.35, issue.1, pp.343-389, 2009.

R. Sekar, I. V. Ramakrishnan, and A. Voronkov, Term Indexing, pp.1853-1964, 2001.
DOI : 10.1016/B978-044450813-3/50028-X

J. Seligman, A cut-free sequent calculus for elementary situated reasoning, 1991.

J. Seligman, Internalization: The Case of Hybrid Logics, Journal of Logic and Computation, vol.11, issue.5, pp.671-689, 2001.
DOI : 10.1093/logcom/11.5.671

J. Seligman, The Logic of Correct Description, Advances in Intensional Logic, Applied Logic Series, pp.107-135, 1997.
DOI : 10.1007/978-94-015-8879-9_5

B. Cate, Model theory for extended modal languages, ILLC Dissertation Series DS-2005-01. 1.2.3, 2005.

M. Tzakova, Tableau Calculi for Hybrid Logics, Proceedings of the Conference on Tableaux Calculi and Related Methods (TABLEAUX), pp.278-292, 1999.
DOI : 10.1007/3-540-48754-9_24

J. Van-benthem, Modal Correspondence Theory, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, 1976.

M. Vardi, 17 Automata-theoretic techniques for temporal reasoning, pp.971-990, 2006.
DOI : 10.1016/S1570-2464(07)80020-6

M. Vardi, Why is modal logic so robustly decidable?, Descriptive Complexity and Finite Models, pp.149-184, 1996.
DOI : 10.1090/dimacs/031/05

A. Voronkov, Algorithms, Datastructures, and other Issues in Efficient Automated Deduction, Proceedings of IJCAR 2001, number 2083 in LNAI, pp.13-28, 2001.
DOI : 10.1007/3-540-45744-5_3

C. Weidenbach, Combining Superposition, Sorts and Splitting, pp.1965-2014, 2001.
DOI : 10.1016/B978-044450813-3/50029-1

C. Weidenbach, R. Schmidt, T. Hillenbrand, R. Rusev, and D. Topic, System Description: Spass Version 3.0, Proc. of CADE-21, number 4603 in Lecture Notes in Artificial Intelligence, pp.514-520, 2007.
DOI : 10.1007/978-3-540-73595-3_38