1: \begin{thebibliography}{10}
2:
3: \bibitem{arec:tree00}
4: C.~Areces, R.~Gennari, J.~Heguiabehere, and M.~de~Rijke.
5: \newblock Tree-based heuristics in modal theorem proving.
6: \newblock In W.~Horn, editor, {\em Proc. of {ECAI2000}}, Berlin, Germany, 2000. IOS Press
7: Amsterdam.
8:
9: \bibitem{BaaderSattler-StudiaLogica-2000}
10: F.~Baader and U.~Sattler.
11: \newblock An overview of tableau algorithms for description logics.
12: \newblock {\em Studia Logica}, 69:5--40, 2001.
13:
14: \bibitem{BaaderTobies-LTCS-01-03}
15: F.~Baader and S.~Tobies.
16: \newblock The inverse method implements the automata approach for modal
17: satisfiability.
18: \newblock LTCS-Report 01-03, LuFG Theoretical Computer Science, RWTH Aachen,
19: Germany, 2001.
20: \newblock See http://www-lti.informatik.rwth-aachen.de/Forschung/Reports.html.
21:
22: \bibitem{blackburn01:_modal_logic}
23: P.~Blackburn, M.~de~Rijke, and Y.~Venema.
24: \newblock {\em Modal Logic}.
25: \newblock Cambridge University Press, 2001.
26: \newblock Publishing date May 2001, preliminary version available online from
27: \url{http://www.mlbook.org/}.
28:
29: \bibitem{lncs531*233}
30: C.~Courcoubetis, M.~Vardi, P.~Wolper, and M.~Yannakakis.
31: \newblock Memory efficient algorithms for the verification of temporal
32: properties.
33: \newblock In E.~M. Clarke and R.~P. Kurshan, editors, {\em Proc. of
34: {CAV} '90}, volume 531 of LNCS, pages 233--242. Springer Verlag, 1991.
35:
36: \bibitem{donini00:_exptim_alc}
37: F.~M. Donini and F.~Massacci.
38: \newblock {EXPTIME} tableaux for {ALC}.
39: \newblock {\em Artificial Intelligence}, 124(1):87--138, 2000.
40:
41: \bibitem{dowling84:_linear_time_testin_horn}
42: W.~F. Dowling and J.~H. Gallier.
43: \newblock Linear-time algorithms for testing the satisfiability of
44: propositional horn formulae.
45: \newblock {\em Journal of Logic Programming}, 1(3):267--28, 1984.
46:
47: \bibitem{Proc:Tableaux2000}
48: R.~Dyckhoff, editor.
49: \newblock {\em Proc. of {TABLEAUX 2000}},
50: number 1847 in LNAI, St Andrews,
51: Scotland, UK, 2000. Springer Verlag.
52:
53: \bibitem{GPVW95}
54: R.~Gerth, D.~Peled, M.~Vardi, and P.~Wolper.
55: \newblock Simple on-the-fly automatic verification of linear temporal logic.
56: \newblock In {\em Proc. of the 15th International Symposium on Protocol
57: Specification, Testing, and Verification}, pages 3--18, Warsaw, Poland, 1995.
58: Chapman \& Hall.
59:
60: \bibitem{Gore-Tableau-Handbook-1998}
61: R.~Gor{\'e}.
62: \newblock Tableau methods for modal and temporal logics.
63: \newblock In M.~D'Agostino, D.~M. Gabbay, R.~H{\"a}hnle, and J.~Posegga,
64: editors, {\em Handbook of Tableau Methods}. Kluwer, Dordrecht, 1998.
65:
66: \bibitem{Horrocks-Tableaux-2000}
67: I.~Horrocks.
68: \newblock Benchmark analysis with {FaCT}.
69: \newblock In Dyckhoff \cite{Proc:Tableaux2000}, pages 62--66.
70:
71: \bibitem{HustadtSchmidt-Tableaux2000}
72: U.~Hustadt and R.~A. Schmidt.
73: \newblock {MSPASS}: Modal reasoning by translation and first-order resolution.
74: \newblock In Dyckhoff \cite{Proc:Tableaux2000}, pages 67--71.
75:
76: \bibitem{ladner:1977a}
77: R.~E. Ladner.
78: \newblock The computational complexity of provability in systems of modal
79: propositional logic.
80: \newblock {\em {SIAM} Journal on Computing}, 6(3):467--480, 1977.
81:
82: \bibitem{LutzSattlerAIML00}
83: C.~Lutz and U.~Sattler.
84: \newblock The complexity of reasoning with boolean modal logic.
85: \newblock In Wolter F., H.~Wansing, M.~de~Rijke, and M.~Zakharyaschev, editors,
86: {\em Preliminary Proc. of {AiML2000}}, Leipzig, Germany, 2000.
87:
88: \bibitem{Schmidt98f}
89: R.~A. Schmidt.
90: \newblock Resolution is a decision procedure for many propositional modal
91: logics.
92: \newblock In M.~Kracht, M.~de~Rijke, H.~Wansing, and M.~Zakharyaschev, editors,
93: {\em Advances in Modal Logic, Volume 1}, volume~87 of {\em Lecture Notes},
94: pages 189--208. CSLI Publications, Stanford, 1998.
95:
96: \bibitem{Spaan93a}
97: E.~Spaan.
98: \newblock {\em Complexity of Modal Logics}.
99: \newblock PhD thesis, Univ. van Amsterdam, 1993.
100:
101: %\bibitem{spaan_e:1993a}
102: %E.~Spaan.
103: %\newblock The complexity of propositional tense logics.
104: %\newblock In M.~de~Rijke, editor, {\em Diamonds and Defaults}, pages 287--307.
105: % Kluwer Academic Publishers, 1993.
106:
107: \bibitem{VaWo86}
108: Moshe~Y. Vardi and Pierre Wolper.
109: \newblock Automata-theoretic techniques for modal logics of programs.
110: \newblock {\em Journal of Computer and System Sciences}, 32:183--221, 1986.
111:
112: \bibitem{vardi94:_reason_infin_comput}
113: M.Y. Vardi and P.~Wolper.
114: \newblock Reasoning about infinite computations.
115: \newblock {\em Information and Computation}, 115:1--37, 1994.
116:
117: \bibitem{Voronkov-ToCL-2001}
118: A.~Voronkov.
119: \newblock How to optimize proof-search in modal logics: new methods of proving
120: redundancy criteria for sequent calculi.
121: \newblock {\em {ACM} Transactions on Computational Logic}, 1(4), 2001. Available
122: online from \url{http://www.cs.man.ac.uk/~voronkov/recent.html} .
123:
124: \end{thebibliography}
125: