Modal Languages and Bounded Fragments of Predicate Logic, Journal of Philosophical Logic, vol.60, issue.5, pp.217-274, 1998. ,
DOI : 10.2307/2275853
Logic Engineering. The Case of Description and Hybrid Logics, 2000. ,
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
Hybrid logics, pp.821-868, 2006. ,
URL : https://hal.archives-ouvertes.fr/inria-00549320
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
Tree-based heuristics in modal theorem proving, Proc. of ECAI'2000, pp.199-203, 2000. ,
URL : https://hal.archives-ouvertes.fr/inria-00000338
Abstract, The Journal of Symbolic Logic, vol.XLI, issue.03, pp.977-1010, 2001. ,
DOI : 10.1093/jigpal/8.5.653
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
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
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
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
Strategies for modal resolution: Results and problems, Journal of Automated Reasoning, vol.4, issue.1, pp.1-38, 1990. ,
DOI : 10.1007/BF00302639
Term Rewriting and All That, 1998. ,
Resolution Theorem Proving, pp.19-99, 2001. ,
DOI : 10.1016/B978-044450813-3/50004-7
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
The lambda calculus: its syntax and semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984. ,
Internalizing labelled deduction, Journal of Logic and Computation, vol.10, issue.1, pp.137-168, 2000. ,
DOI : 10.1093/logcom/10.1.137
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
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
Modal Logic, volume 53 of Cambridge Tracts in Theoretical Computer Sciene ,
Handbook of Modal Logics, volume 3 of Studies in Logic and Practical Reasoning, 2006. ,
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
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
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
Proving Theorems with the Modification Method, SIAM Journal on Computing, vol.4, issue.4, pp.412-430, 1975. ,
DOI : 10.1137/0204036
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
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
Model checking, 1999. ,
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
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
Modal resolution in clausal form, Theoretical Computer Science, vol.65, issue.1, pp.1-33, 1989. ,
DOI : 10.1016/0304-3975(89)90137-0
Linear modal deductions, Proc. of the 9th Conference on Automated Deduction, pp.487-499, 1988. ,
DOI : 10.1007/BFb0012851
Propositional dynamic logic of regular programs, Journal of Computer and System Sciences, vol.18, issue.11, pp.194-211, 1979. ,
Destructive Modal Resolution, Journal of Logic and Computation, vol.1, issue.1, pp.83-97, 1990. ,
DOI : 10.1093/logcom/1.1.83
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
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
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
Axiomatic classes in propositional modal logic, Algebra and Logic, pp.163-173, 1975. ,
DOI : 10.1016/S0049-237X(08)70723-7
Why are modal logics so robustly decidable, Current Trends in Theoretical Computer Science. Entering the 21st Century, pp.393-408, 2001. ,
Dynamic logic. Foundations of Computing, 2000. ,
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
Recherches sur la théorie de la démonstrations, Logical Writings. Reidel, 1930. ,
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
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
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
A tutorial on (co)algebras and (co)induction, EATCS Bulletin, vol.62, issue.33, pp.222-259, 1997. ,
Resolution Strategies as Decision Procedures, Journal of the ACM, vol.23, issue.3, pp.398-417 ,
DOI : 10.1145/321958.321960
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
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
Simple Word Problems in Universal Algebras, Computational Algebra, pp.263-297, 1970. ,
DOI : 10.1007/978-3-642-81955-1_23
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
Mathematical logic and Hilbert's -symbol, 1969. ,
A Survey of Symbolic Logic Reprint of Chapters I?IV by, 1918. ,
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
Experiments in automated deduction with condensed detachment, CADE-11: Proceedings of the 11th International Conference on Automated Deduction, pp.209-223, 1992. ,
Applying 'design by contract', Computer, vol.25, issue.10, pp.40-51, 1992. ,
DOI : 10.1109/2.161279
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
Resolution calculi for modal logics, Eight Papers Translated from the Russian, pp.1-14, 1989. ,
DOI : 10.1090/trans2/143/01
On languages with two variables, Mathematical Logic Quarterly, vol.27, issue.1, 1975. ,
DOI : 10.1002/malq.19750210118
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
Basic superposition is complete, Proc. of the 4th European Symposium on Programming, pp.371-389, 1992. ,
DOI : 10.1007/3-540-55253-7_22
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
Computing Small Clause Normal Forms, pp.335-367, 2001. ,
DOI : 10.1016/B978-044450813-3/50008-4
A resolution calculus for modal logics, Proc. of the 9th Conference on Automated Deduction, pp.500-516, 1988. ,
DOI : 10.1007/BFb0012852
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
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
Encoding twovalued non-classical logics in classical logic, pp.1403-1486, 2001. ,
DOI : 10.1016/b978-044450813-3/50023-0
Models of program logics, 20th Annual Symposium on Foundations of Computer Science (sfcs 1979), pp.115-122, 1979. ,
DOI : 10.1109/SFCS.1979.24
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
Paramodulation and theorem-proving in firstorder, Machine Intelligence, vol.4, issue.21, pp.135-150, 1969. ,
DOI : 10.1142/9789812813411_0008
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
Logic for mathematicians, 1953. ,
On the origins of bisimulation and coinduction, ACM Transactions on Programming Languages and Systems, vol.31, issue.4, 2002. ,
Decidability by resolution for propositional modal logics, Journal of Automated Reasoning, vol.22, issue.4, pp.379-396, 1999. ,
DOI : 10.1023/A:1006043519663
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. ,
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. ,
Term Indexing, pp.1853-1964, 2001. ,
DOI : 10.1016/B978-044450813-3/50028-X
A cut-free sequent calculus for elementary situated reasoning, 1991. ,
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
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
Model theory for extended modal languages, ILLC Dissertation Series DS-2005-01. 1.2.3, 2005. ,
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
Modal Correspondence Theory, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, 1976. ,
17 Automata-theoretic techniques for temporal reasoning, pp.971-990, 2006. ,
DOI : 10.1016/S1570-2464(07)80020-6
Why is modal logic so robustly
decidable?, Descriptive Complexity and Finite Models, pp.149-184, 1996. ,
DOI : 10.1090/dimacs/031/05
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
Combining Superposition, Sorts and Splitting, pp.1965-2014, 2001. ,
DOI : 10.1016/B978-044450813-3/50029-1
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