1: \begin{thebibliography}{}
2:
3: \bibitem[\protect\BCAY{Abiteboul, Hull, \BBA\ Vianu}{Abiteboul
4: et~al.}{1995}]{abiteboul95:_found_datab}
5: Abiteboul, S., Hull, R., \BBA\ Vianu, V. \BBOP1995\BBCP.
6: \newblock {\Bem Foundations of Databases}.
7: \newblock Addison Wesley.
8:
9: \bibitem[\protect\BCAY{Andr\'eka, van Benthem, \BBA\ N\'emeti}{Andr\'eka
10: et~al.}{1998}]{AndrekaBenNem98}
11: Andr\'eka, H., van Benthem, J., \BBA\ N\'emeti, I. \BBOP1998\BBCP.
12: \newblock \BBOQ Modal languages and bounded fragments of predicate logic\BBCQ\
13: \newblock {\Bem Journal of Philosophical Logic}, {\Bem 27}, 217--274.
14:
15: \bibitem[\protect\BCAY{Areces}{Areces}{2000}]{areces00:_logic_engin}
16: Areces, C. \BBOP2000\BBCP.
17: \newblock {\Bem Logic Engineering: The Case of Description and Hybrid Logics}.
18: \newblock Ph.D.\ thesis, University of Amsterdam.
19:
20: \bibitem[\protect\BCAY{Areces, Blackburn, \BBA\ Marx}{Areces
21: et~al.}{2000}]{ArecesBlackburnMarx-JSL-2000}
22: Areces, C., Blackburn, P., \BBA\ Marx, M. \BBOP2000\BBCP.
23: \newblock \BBOQ Hybrid logics: Characterization, interpolation, and
24: complexity\BBCQ\
25: \newblock {\Bem Journal of Symbolic Logic}.
26: \newblock To appear.
27:
28: \bibitem[\protect\BCAY{Areces \BBA\ de~Rijke}{Areces \BBA\
29: de~Rijke}{2000}]{ArecesDeRijkeAIML00}
30: Areces, C.\BBACOMMA\ \BBA\ de~Rijke, M. \BBOP2000\BBCP.
31: \newblock \BBOQ Description and/or hybrid logics\BBCQ\
32: \newblock In Wolter, F., Wansing, H., de~Rijke, M., \BBA\ Zakharyaschev,
33: M.\BEDS, {\Bem Preliminary Proceedings of the Workshop Advances in Modal
34: Logics {(AiML2000)}}\ Leipzig, Deutschland.
35:
36: \bibitem[\protect\BCAY{Areces, Gennari, Heguiabehere, \BBA\ de~Rijke}{Areces
37: et~al.}{2000}]{arec:tree00}
38: Areces, C., Gennari, R., Heguiabehere, J., \BBA\ de~Rijke, M. \BBOP2000\BBCP.
39: \newblock \BBOQ Tree-based heuristics in modal theorem proving\BBCQ\
40: \newblock In Horn, W.\BED, {\Bem Proceedings of the 14th European Conference on
41: Artificial Intelligence {(ECAI2000)}}\ Berlin, Germany. IOS Press Amsterdam.
42:
43: \bibitem[\protect\BCAY{Areces, Blackburn, \BBA\ Marx}{Areces
44: et~al.}{1999}]{areces:_road_map_compl_hybrid_logic}
45: Areces, C., Blackburn, P., \BBA\ Marx, M. \BBOP1999\BBCP.
46: \newblock \BBOQ A road-map on complexity for hybrid logics\BBCQ\
47: \newblock In Flum, J.\BBACOMMA\ \BBA\ Rodr{\'i}guez-Artalejo, M.\BEDS, {\Bem
48: Proceedings of the Annual Conference of the European Association for Computer
49: Science Logic {(CSL-99)}}, \lowercase{\BNUM}\ 1683 in Lecture Notes in
50: Computer Science, \BPGS\ 307--321\ Madrid, Spain. Springer Verlag.
51:
52: \bibitem[\protect\BCAY{Baader}{Baader}{1991}]{Baader91c}
53: Baader, F. \BBOP1991\BBCP.
54: \newblock \BBOQ Augmenting concept languages by transitive closure of roles: An
55: alternative to terminological cycles\BBCQ\
56: \newblock In J.~Mylopoulos, R.~R.\BED, {\Bem Proceedings of the 12th
57: International Joint Conference on Artificial Intelligence {(IJCAI-91)}},
58: \BPGS\ 446--451\ Sydney, Australia. Morgan Kaufman Publishers, Inc.
59:
60: \bibitem[\protect\BCAY{Baader, Buchheit, \BBA\ Hollunder}{Baader
61: et~al.}{1996}]{BaaderBuchheit+-AIJ-1996}
62: Baader, F., Buchheit, M., \BBA\ Hollunder, B. \BBOP1996\BBCP.
63: \newblock \BBOQ Cardinality restrictions on concepts\BBCQ\
64: \newblock {\Bem Artificial Intelligence}, {\Bem 88\/}(1--2), 195--213.
65:
66: \bibitem[\protect\BCAY{Baader, B\"urckert, Nebel, Nutt, \BBA\ Smolka}{Baader
67: et~al.}{1993}]{BBNNS93}
68: Baader, F., B\"urckert, H.-J., Nebel, B., Nutt, W., \BBA\ Smolka, G.
69: \BBOP1993\BBCP.
70: \newblock \BBOQ On the expressivity of feature logics with negation, functional
71: uncertainty, and sort equations\BBCQ\
72: \newblock {\Bem Journal of Logic, Language and Information}, {\Bem 2}, 1--18.
73:
74: \bibitem[\protect\BCAY{Baader, Franconi, Hollunder, Nebel, \BBA\
75: Profitlich}{Baader et~al.}{1994}]{BaaderFranconi+-OptJournal-94}
76: Baader, F., Franconi, E., Hollunder, B., Nebel, B., \BBA\ Profitlich, H.
77: \BBOP1994\BBCP.
78: \newblock \BBOQ An empirical analysis of optimization techniques for
79: terminological representation systems or: Making {KRIS} get a move on\BBCQ\
80: \newblock {\Bem Applied Artificial Intelligence. Special Issue on Knowledge
81: Base Management}, {\Bem 4}, 109--132.
82:
83: \bibitem[\protect\BCAY{Baader \BBA\ Hanschke}{Baader \BBA\
84: Hanschke}{1993}]{BaaderHanschke-GWAI-92}
85: Baader, F.\BBACOMMA\ \BBA\ Hanschke, P. \BBOP1993\BBCP.
86: \newblock \BBOQ Extensions of concept languages for a mechanical engineering
87: application\BBCQ\
88: \newblock In {\Bem Proceedings of the 16th German AI-Conference, {GWAI-92}},
89: \lowercase{\BVOL}\ 671 of {\Bem Lecture Notes in Computer Science}, \BPGS\
90: 132--143\ Bonn (Germany). Springer Verlag.
91:
92: \bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\
93: Hollunder}{1991}]{BaaderHollunder-SIGART-91}
94: Baader, F.\BBACOMMA\ \BBA\ Hollunder, B. \BBOP1991\BBCP.
95: \newblock \BBOQ {KRIS}: Knowledge representation and inference system, system
96: description\BBCQ\
97: \newblock {\Bem ACM SIGART Bulletin}, {\Bem 2}, 8--14.
98:
99: \bibitem[\protect\BCAY{Baader, McGuiness, Nardi, \BBA\ Patel-Schneider}{Baader
100: et~al.}{2001}]{baader01:_descr_logic_handb}
101: Baader, F., McGuiness, D., Nardi, D., \BBA\ Patel-Schneider, P.\BEDS.
102: \BBOP2001\BBCP.
103: \newblock {\Bem The Description Logic Handbook: Theory, Implementation and
104: Applications}.
105: \newblock Cambridge University Press.
106: \newblock forthcoming.
107:
108: \bibitem[\protect\BCAY{Baader \BBA\ Sattler}{Baader \BBA\
109: Sattler}{1999}]{BaaderSattler-JLC-99}
110: Baader, F.\BBACOMMA\ \BBA\ Sattler, U. \BBOP1999\BBCP.
111: \newblock \BBOQ Expressive number restrictions in description logics\BBCQ\
112: \newblock {\Bem Journal for Logic and Computation}, {\Bem 9\/}(3), 319--350.
113:
114: \bibitem[\protect\BCAY{Baader \BBA\ Sattler}{Baader \BBA\
115: Sattler}{2000}]{BaaderSattler-StudiaLogica-2000}
116: Baader, F.\BBACOMMA\ \BBA\ Sattler, U. \BBOP2000\BBCP.
117: \newblock \BBOQ An overview of tableau algorithms for description logics\BBCQ\
118: \newblock {\Bem Studia Logica}.
119: \newblock To appear.
120:
121: \bibitem[\protect\BCAY{Bechhofer \BBA\ Horrocks}{Bechhofer \BBA\
122: Horrocks}{2000}]{bechhofer:_drivin_user_inter_fact}
123: Bechhofer, S.\BBACOMMA\ \BBA\ Horrocks, I. \BBOP2000\BBCP.
124: \newblock \BBOQ Driving user interfaces from {FaCT}\BBCQ\
125: \newblock In Baader, F.\BBACOMMA\ \BBA\ Sattler, U.\BEDS, {\Bem Proceedings of
126: the 2000 International Workshop on Description Logics {(DL2000)}},
127: \lowercase{\BVOL}~33 of {\Bem CEUR Workshop Proceedings}, \BPGS\ 45--54\ RWTH
128: Aachen, Germany.
129: \newblock Available online from
130: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-33/}.
131:
132: \bibitem[\protect\BCAY{Berger}{Berger}{1966}]{berger66:_undecidability_dominoe%
133: _problem}
134: Berger, R. \BBOP1966\BBCP.
135: \newblock \BBOQ The undecidability of the dominoe problem\BBCQ\
136: \newblock {\Bem Memoirs of the American Mathematical Society}, {\Bem 66},
137: 1--17.
138:
139: \bibitem[\protect\BCAY{Berners-Lee}{Berners-Lee}{1999}]{berners-lee99:_weavin_%
140: web}
141: Berners-Lee, T. \BBOP1999\BBCP.
142: \newblock {\Bem Weaving the Web}.
143: \newblock Harper, San Francisco.
144:
145: \bibitem[\protect\BCAY{Blackburn \BBA\ Seligman}{Blackburn \BBA\
146: Seligman}{1995}]{blackburn95:_hybrid_languages}
147: Blackburn, P.\BBACOMMA\ \BBA\ Seligman, J. \BBOP1995\BBCP.
148: \newblock \BBOQ Hybrid languages\BBCQ\
149: \newblock {\Bem Journal of Logic, Language and Information}, {\Bem 3\/}(4),
150: 251--272.
151:
152: \bibitem[\protect\BCAY{B{\"o}rger, Gr{\"a}del, \BBA\ Gurevich}{B{\"o}rger
153: et~al.}{1997}]{BoGrGu97}
154: B{\"o}rger, E., Gr{\"a}del, E., \BBA\ Gurevich, Y. \BBOP1997\BBCP.
155: \newblock {\Bem {The Classical Decision Problem}}.
156: \newblock Springer Verlag.
157:
158: \bibitem[\protect\BCAY{Borgida}{Borgida}{1995}]{Borg95}
159: Borgida, A. \BBOP1995\BBCP.
160: \newblock \BBOQ Description logics in data management\BBCQ\
161: \newblock {\Bem Transaction on Knowledge and Data Engineering}, {\Bem 7\/}(5),
162: 671--682.
163:
164: \bibitem[\protect\BCAY{Borgida}{Borgida}{1996}]{Borgida96a}
165: Borgida, A. \BBOP1996\BBCP.
166: \newblock \BBOQ On the relative expressiveness of description logics and first
167: order logics\BBCQ\
168: \newblock {\Bem Artificial Intelligence}, {\Bem 82}, 353--367.
169:
170: \bibitem[\protect\BCAY{Borgida \BBA\ Patel-Schneider}{Borgida \BBA\
171: Patel-Schneider}{1994}]{Borgida94}
172: Borgida, A.\BBACOMMA\ \BBA\ Patel-Schneider, P.~F. \BBOP1994\BBCP.
173: \newblock \BBOQ A semantics and complete algorithm for subsumption in the
174: \textsc{Classic} description logic\BBCQ\
175: \newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1},
176: 277--308.
177:
178: \bibitem[\protect\BCAY{Brachman \BBA\ Levesque}{Brachman \BBA\
179: Levesque}{1984}]{brachman84:_tract_subsum_frame_based_descr_languag}
180: Brachman, R.~J.\BBACOMMA\ \BBA\ Levesque, H.~J. \BBOP1984\BBCP.
181: \newblock \BBOQ The tractability of subsumption in frame-based description
182: languages\BBCQ\
183: \newblock In {\Bem Proceedings of the 4th National Conference on Artificial
184: Intelligence {(AAAI-84)}}, \BPGS\ 34--37\ Austin, TX, USA. AAAI Press.
185:
186: \bibitem[\protect\BCAY{Brachman \BBA\ Levesque}{Brachman \BBA\
187: Levesque}{1985}]{brachman85:_readin_knowl_repres}
188: Brachman, R.~J.\BBACOMMA\ \BBA\ Levesque, H.~J.\BEDS. \BBOP1985\BBCP.
189: \newblock {\Bem Readings in Knowledge Representation}.
190: \newblock Morgan Kaufman Publishers, Inc., Los Altos.
191:
192: \bibitem[\protect\BCAY{Brachman, McGuinness, Patel-Schneider, Resnick, \BBA\
193: Borgida}{Brachman et~al.}{1991}]{BMPAB91}
194: Brachman, R.~J., McGuinness, D.~L., Patel-Schneider, P.~F., Resnick, L.~A.,
195: \BBA\ Borgida, A. \BBOP1991\BBCP.
196: \newblock \BBOQ Living with {CLASSIC}: When and how to use a {KL-ONE}-like
197: language\BBCQ\
198: \newblock In Sowa, J.~F.\BED, {\Bem Principles of Semantic Networks}, \BPGS\
199: 401--456. Morgan Kaufman Publishers, Inc.
200:
201: \bibitem[\protect\BCAY{Brachman \BBA\ Schmolze}{Brachman \BBA\
202: Schmolze}{1985}]{brachman85:_overv_kl_one_knowl_repres_system}
203: Brachman, R.~J.\BBACOMMA\ \BBA\ Schmolze, J.~G. \BBOP1985\BBCP.
204: \newblock \BBOQ An overview of the {KL-ONE} knowledge representation
205: system\BBCQ\
206: \newblock {\Bem Cognitive Science}, {\Bem 9\/}(2), 171--216.
207:
208: \bibitem[\protect\BCAY{Bresciani, Franconi, \BBA\ Tessaris}{Bresciani
209: et~al.}{1995}]{BrFT95}
210: Bresciani, P., Franconi, E., \BBA\ Tessaris, S. \BBOP1995\BBCP.
211: \newblock \BBOQ Implementing and testing expressive description logics:
212: Preliminary report\BBCQ\
213: \newblock In Borgida, A., Lenzerini, M., Nardi, D., \BBA\ Nebel, B.\BEDS, {\Bem
214: Working Notes of the 1995 Description Logics Workshop}, Technical Report, RAP
215: 07.95, Dipartimento di Informatica e Sistemistica, \BPGS\ 131--139\ Rome
216: (Italy).
217:
218: \bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit
219: et~al.}{1993}]{Buchheit93}
220: Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993\BBCP.
221: \newblock \BBOQ Decidable reasoning in terminological knowledge representation
222: systems\BBCQ\
223: \newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1},
224: 109--138.
225:
226: \bibitem[\protect\BCAY{Calvanese, {De~Giacomo}, \BBA\ Lenzerini}{Calvanese
227: et~al.}{1999}]{CaDL99}
228: Calvanese, D., {De~Giacomo}, G., \BBA\ Lenzerini, M. \BBOP1999\BBCP.
229: \newblock \BBOQ Reasoning in expressive description logics with fixpoints based
230: on automata on infinite trees\BBCQ\
231: \newblock In Dean, T.\BED, {\Bem Proceedings of the 16th International Joint
232: Conference on Artificial Intelligence {(IJCAI-99)}}, \BPGS\ 84--89\
233: Stockholm, Sweden. Morgan Kaufman Publishers, Inc.
234:
235: \bibitem[\protect\BCAY{Calvanese, {De~Giacomo}, Lenzerini, Nardi, \BBA\
236: Rosati}{Calvanese et~al.}{1998}]{CDLNR98}
237: Calvanese, D., {De~Giacomo}, G., Lenzerini, M., Nardi, D., \BBA\ Rosati, R.
238: \BBOP1998\BBCP.
239: \newblock \BBOQ Description logic framework for information integration\BBCQ\
240: \newblock In Cohn, A.~G., Schubert, L., \BBA\ Shapiro, S.~C.\BEDS, {\Bem
241: Principles of Knowledge Representation and Reasoning, Proceedings of the 6th
242: International Conference {(KR'98)}}, \BPGS\ 2--13\ Trento, Italy. Morgan
243: Kaufman Publishers, Inc.
244:
245: \bibitem[\protect\BCAY{Calvanese, {De~Giacomo}, \BBA\ Rosati}{Calvanese
246: et~al.}{1999}]{calvanese99:_data_integ}
247: Calvanese, D., {De~Giacomo}, G., \BBA\ Rosati, R. \BBOP1999\BBCP.
248: \newblock \BBOQ Data integration and reconciliation in data warehousing\BBCQ\
249: \newblock {\Bem Network and Information Systems}, {\Bem 4\/}(2), 413--432.
250:
251: \bibitem[\protect\BCAY{Calvanese, Lenzerini, \BBA\ Nardi}{Calvanese
252: et~al.}{1994}]{CalvLenzNardi-KR-1994}
253: Calvanese, D., Lenzerini, M., \BBA\ Nardi, D. \BBOP1994\BBCP.
254: \newblock \BBOQ A unified framework for class based representation
255: formalism\BBCQ\
256: \newblock In Doyle, J., Sandewall, E., \BBA\ Torasso, P.\BEDS, {\Bem Principles
257: of Knowledge Representation and Reasoning, Proceedings of the 4th
258: International Conference {(KR'94)}}, \BPGS\ 109--120\ Bonn, Germany. Morgan
259: Kaufman Publishers, Inc.
260:
261: \bibitem[\protect\BCAY{Calvanese, Lenzerini, \BBA\ Nardi}{Calvanese
262: et~al.}{1998}]{CaLN98}
263: Calvanese, D., Lenzerini, M., \BBA\ Nardi, D. \BBOP1998\BBCP.
264: \newblock \BBOQ Description logics for conceptual data modeling\BBCQ\
265: \newblock In Chomicki, J.\BBACOMMA\ \BBA\ Saake, G.\BEDS, {\Bem Logics for
266: Databases and Information Systems}, \BPGS\ 229--264. Kluwer Academic
267: Publisher.
268:
269: \bibitem[\protect\BCAY{{De~Giacomo}}{{De~Giacomo}}{1995}]{DeGiacomo95a}
270: {De~Giacomo}, G. \BBOP1995\BBCP.
271: \newblock {\Bem Decidability of Class-Based Knowledge Representation
272: Formalisms}.
273: \newblock Ph.D.\ thesis, Dipartimento di Informatica e Sistemistica,
274: Universit{\`a}\ di Roma ``La Sapienza''.
275:
276: \bibitem[\protect\BCAY{{{De~Giacomo}} \BBA\ Lenzerini}{{{De~Giacomo}} \BBA\
277: Lenzerini}{1994a}]{DeLe94}
278: {{De~Giacomo}}, G.\BBACOMMA\ \BBA\ Lenzerini, M. \BBOP1994a\BBCP.
279: \newblock \BBOQ Boosting the correspondence between description logics and
280: propositional dynamic logics\BBCQ\
281: \newblock In Hayes-Roth, B.\BBACOMMA\ \BBA\ Korf, R.~E.\BEDS, {\Bem
282: Proceedings of the 12th National Conference on Artificial Intelligence
283: {(AAAI-94)}}, \BPGS\ 205--212\ Seattle, Washington, USA. AAAI Press.
284:
285: \bibitem[\protect\BCAY{{{De~Giacomo}} \BBA\ Lenzerini}{{{De~Giacomo}} \BBA\
286: Lenzerini}{1994b}]{GiLe94}
287: {{De~Giacomo}}, G.\BBACOMMA\ \BBA\ Lenzerini, M. \BBOP1994b\BBCP.
288: \newblock \BBOQ A concept language with number restrictions and fixpoints, and
289: its relationship with $\mu$-calculus\BBCQ\
290: \newblock In Cohn, A.~G.\BED, {\Bem Proceedings of the 11th European Conference
291: on Artificial Intelligence {(ECAI'94)}}\ Amsterdam, The Netherlands. John
292: Wiley and Sons.
293:
294: \bibitem[\protect\BCAY{{De~Giacomo} \BBA\ Lenzerini}{{De~Giacomo} \BBA\
295: Lenzerini}{1994c}]{DeLe94c}
296: {De~Giacomo}, G.\BBACOMMA\ \BBA\ Lenzerini, M. \BBOP1994c\BBCP.
297: \newblock \BBOQ Description logics with inverse roles, functional restrictions,
298: and n-ary relations\BBCQ\
299: \newblock In MacNish, C., Pearce, D., \BBA\ Pereira, L.~M.\BEDS, {\Bem 1994
300: European Workshop on Logic in Artificial Intelligence {(JELIA'94)}},
301: \lowercase{\BNUM}\ 838 in Lecture Notes in Artificial Intelligence, \BPGS\
302: 332--346\ York, UK. Springer Verlag.
303:
304: \bibitem[\protect\BCAY{{De~Giacomo} \BBA\ Lenzerini}{{De~Giacomo} \BBA\
305: Lenzerini}{1996}]{DeGiacomo96a}
306: {De~Giacomo}, G.\BBACOMMA\ \BBA\ Lenzerini, M. \BBOP1996\BBCP.
307: \newblock \BBOQ Tbox and abox reasoning in expressive description logics\BBCQ\
308: \newblock In Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.\BEDS, {\Bem Principles
309: of Knowledge Representation and Reasoning, Proceedings of the 5th
310: International Conference {(KR'96)}}, \BPGS\ 316--327\ Cambridge,
311: Massachusetts, USA. Morgan Kaufman Publishers, Inc.
312:
313: \bibitem[\protect\BCAY{{De~Giacomo} \BBA\ Massacci}{{De~Giacomo} \BBA\
314: Massacci}{2001}]{degiacomo00:_combin_deduc_model_check_tableaux}
315: {De~Giacomo}, G.\BBACOMMA\ \BBA\ Massacci, F. \BBOP2001\BBCP.
316: \newblock \BBOQ Combining deduction and model checking into tableaux and
317: algorithms for converse-{PDL}\BBCQ\
318: \newblock {\Bem Information and Computation}.
319: \newblock To appear.
320:
321: \bibitem[\protect\BCAY{de~Nivelle}{de~Nivelle}{2000}]{nivelle00:_trans_s4_k5_g%
322: f}
323: de~Nivelle, H. \BBOP2000\BBCP.
324: \newblock \BBOQ Translation of {S4} and {K5} into {GF} and {2VAR}\BBCQ\
325: \newblock Unpublished Manuscript.
326:
327: \bibitem[\protect\BCAY{de~Nivelle \BBA\ de~Rijke}{de~Nivelle \BBA\
328: de~Rijke}{2000}]{NivelleRij00}
329: de~Nivelle, H.\BBACOMMA\ \BBA\ de~Rijke, M. \BBOP2000\BBCP.
330: \newblock \BBOQ Deciding the guarded fragments by resolution\BBCQ\
331: \newblock {\Bem Journal for Logic and Computation}.
332: \newblock To appear.
333:
334: \bibitem[\protect\BCAY{Donini, Hollunder, Lenzerini, Spaccamela, Nardi, \BBA\
335: Nutt}{Donini et~al.}{1992}]{DHLM92}
336: Donini, F.~M., Hollunder, B., Lenzerini, M., Spaccamela, A.~M., Nardi, D.,
337: \BBA\ Nutt, W. \BBOP1992\BBCP.
338: \newblock \BBOQ The complexity of existential quantification in concept
339: languages\BBCQ\
340: \newblock {\Bem Artificial Intelligence}, {\Bem 2--3}, 309--327.
341:
342: \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
343: et~al.}{1991a}]{DLNN91}
344: Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1991a\BBCP.
345: \newblock \BBOQ The complexity of concept languages\BBCQ\
346: \newblock In Allen, J., Fikes, R., \BBA\ Sandewall, E.\BEDS, {\Bem Principles
347: of Knowledge Representation and Reasoning, Proceedings of the 2nd
348: International Conference {(KR'91)}}, \BPGS\ 151--162\ Cambridge,
349: Massachusetts, USA. Morgan Kaufman Publishers, Inc.
350:
351: \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
352: et~al.}{1991b}]{DLNN91b}
353: Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1991b\BBCP.
354: \newblock \BBOQ Tractable concept languages\BBCQ\
355: \newblock In J.~Mylopoulos, R.~R.\BED, {\Bem Proceedings of the 12th
356: International Joint Conference on Artificial Intelligence {(IJCAI-91)}},
357: \BPGS\ 458--463\ Sydney, Australia. Morgan Kaufman Publishers, Inc.
358:
359: \bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
360: et~al.}{1997}]{DLNN97}
361: Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1997\BBCP.
362: \newblock \BBOQ The complexity of concept languages\BBCQ\
363: \newblock {\Bem Information and Computation}, {\Bem 134}, 1--58.
364:
365: \bibitem[\protect\BCAY{Donini \BBA\ Massacci}{Donini \BBA\
366: Massacci}{2000}]{donini00:_exptim_alc}
367: Donini, F.~M.\BBACOMMA\ \BBA\ Massacci, F. \BBOP2000\BBCP.
368: \newblock \BBOQ {EXPTIME} tableaux for {ALC}\BBCQ\
369: \newblock {\Bem Artificial Intelligence}, {\Bem 124\/}(1), 87--138.
370:
371: \bibitem[\protect\BCAY{Dowling \BBA\ Gallier}{Dowling \BBA\
372: Gallier}{1984}]{dowling84:_linear_time_testin_horn}
373: Dowling, W.~F.\BBACOMMA\ \BBA\ Gallier, J.~H. \BBOP1984\BBCP.
374: \newblock \BBOQ Linear-time algorithms for testing the satisfiability of
375: propositional horn formulae\BBCQ\
376: \newblock {\Bem Journal of Logic Programming}, {\Bem 1\/}(3), 267--28.
377:
378: \bibitem[\protect\BCAY{Fensel, Horrocks, van Harmelen, Decker, Erdmann, \BBA\
379: Klein}{Fensel et~al.}{2000}]{fensel00:_oil_nutsh}
380: Fensel, D., Horrocks, I., van Harmelen, F., Decker, S., Erdmann, M., \BBA\
381: Klein, M. \BBOP2000\BBCP.
382: \newblock \BBOQ {OIL} in a nutshell\BBCQ\
383: \newblock In {\Bem Proceedings of the European Knowledge Acquisition Conference
384: {(EKAW-2000)}}, \lowercase{\BNUM}\ 1937 in Lecture Notes in Artificial
385: Intelligence, \BPGS\ 1--16. Springer Verlag.
386:
387: \bibitem[\protect\BCAY{Fischer \BBA\ Ladner}{Fischer \BBA\
388: Ladner}{1979}]{fischer79:_propos_dynam_logic_regul_progr}
389: Fischer, M.~J.\BBACOMMA\ \BBA\ Ladner, R.~E. \BBOP1979\BBCP.
390: \newblock \BBOQ Propositional dynamic logic of regular programs\BBCQ\
391: \newblock {\Bem Journal of Computer and System Sciences}, {\Bem 18}, 194--211.
392:
393: \bibitem[\protect\BCAY{Franconi}{Franconi}{1994}]{franconi94:treatment_of_plur%
394: als}
395: Franconi, E. \BBOP1994\BBCP.
396: \newblock \BBOQ A treatment of plurals and plural quantification based on a
397: theory of collections\BBCQ\
398: \newblock {\Bem Minds and Machines}, {\Bem 3\/}(4), 453--474.
399:
400: \bibitem[\protect\BCAY{Franconi, Baader, Sattler, \BBA\ Vassiliadis}{Franconi
401: et~al.}{2000}]{FrancBaadSattvass-DWQ-Buch}
402: Franconi, E., Baader, F., Sattler, U., \BBA\ Vassiliadis, P. \BBOP2000\BBCP.
403: \newblock \BBOQ Multidimensional data models and aggregation\BBCQ\
404: \newblock In Jarke, M., Lenzerini, M., Vassilious, Y., \BBA\ Vassiliadis,
405: P.\BEDS, {\Bem Fundamentals of Data Warehousing}, \BPGS\ 87--106.
406: Springer-Verlag.
407:
408: \bibitem[\protect\BCAY{Franconi \BBA\ Ng}{Franconi \BBA\
409: Ng}{2000}]{FranconiNg-KRDB-2000}
410: Franconi, E.\BBACOMMA\ \BBA\ Ng, G. \BBOP2000\BBCP.
411: \newblock \BBOQ The i.com tool for intelligent conceptual modeling\BBCQ\
412: \newblock In Bouzeghoub, M., Klusch, M., Nutt, W., \BBA\ Sattler, U.\BEDS,
413: {\Bem Proceedings of the 7th International Workshop on Knowledge
414: Representation meets Databases {(KRDB'99)}}, \lowercase{\BVOL}~29 of {\Bem
415: CEUR Workshop Proceedings}, \BPGS\ 45--53\ Berlin, Germany. RWTH Aachen.
416: \newblock Available online from
417: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-29/}.
418:
419: \bibitem[\protect\BCAY{Ganzinger \BBA\ {de Nivelle}}{Ganzinger \BBA\ {de
420: Nivelle}}{1999}]{GanzNiv99}
421: Ganzinger, H.\BBACOMMA\ \BBA\ {de Nivelle}, H. \BBOP1999\BBCP.
422: \newblock \BBOQ A superposition decision procedure for the guarded fragment
423: with equality\BBCQ\
424: \newblock In {\Bem Proceedings of 14th IEEE Symposium on Logic in Computer
425: Science {(LICS'99)}}, \BPGS\ 295--303\ Trento, Italy. {IEEE} Computer Society
426: Press.
427:
428: \bibitem[\protect\BCAY{Ganzinger, Meyer, \BBA\ Veanes}{Ganzinger
429: et~al.}{1999}]{GanzingerMeyerVeanes-99-lics}
430: Ganzinger, H., Meyer, C., \BBA\ Veanes, M. \BBOP1999\BBCP.
431: \newblock \BBOQ The two-variable guarded fragment with transitive
432: relations\BBCQ\
433: \newblock In {\Bem Proceedings of 14th IEEE Symposium on Logic in Computer
434: Science {(LICS'99)}}, \BPGS\ 25--34\ Trento, Italy. {IEEE} Computer Society
435: Press.
436:
437: \bibitem[\protect\BCAY{Gargov \BBA\ Goranko}{Gargov \BBA\
438: Goranko}{1993}]{gargov93:_modal_logic_with_names}
439: Gargov, G.\BBACOMMA\ \BBA\ Goranko, V. \BBOP1993\BBCP.
440: \newblock \BBOQ Modal logic with names\BBCQ\
441: \newblock {\Bem Journal of Philosophical Logic}, {\Bem 22}, 607--636.
442:
443: \bibitem[\protect\BCAY{G{\'e}cseg \BBA\ Steinby}{G{\'e}cseg \BBA\
444: Steinby}{1984}]{Gecseg-Steinby:84}
445: G{\'e}cseg, F.\BBACOMMA\ \BBA\ Steinby, M. \BBOP1984\BBCP.
446: \newblock {\Bem Tree Automata}.
447: \newblock Akad{\'e}miai Kiad{\'o}, Budapest.
448:
449: \bibitem[\protect\BCAY{Giunchiglia \BBA\ Sebastiani}{Giunchiglia \BBA\
450: Sebastiani}{1996}]{GiunchigliaSeb96b}
451: Giunchiglia, F.\BBACOMMA\ \BBA\ Sebastiani, R. \BBOP1996\BBCP.
452: \newblock \BBOQ A {SAT}-based decision procedure for {ALC}\BBCQ\
453: \newblock In Aiello, L.~C., Doyle, J., \BBA\ Shapiro, S.\BEDS, {\Bem Principles
454: of Knowledge Representation and Reasoning, Proceedings of the 5th
455: International Conference {(KR'96)}}\ Cambridge, Massachusetts, USA. Morgan
456: Kaufman Publishers, Inc.
457:
458: \bibitem[\protect\BCAY{Golumbic}{Golumbic}{1980}]{Go80}
459: Golumbic, M. \BBOP1980\BBCP.
460: \newblock {\Bem Algorithmic Graph Theory and Perfect Graphs}.
461: \newblock Academic Press, New York, NY.
462:
463: \bibitem[\protect\BCAY{Goncalves \BBA\ Gr{\"a}del}{Goncalves \BBA\
464: Gr{\"a}del}{2000}]{GoncalvesGra00}
465: Goncalves, E.\BBACOMMA\ \BBA\ Gr{\"a}del, E. \BBOP2000\BBCP.
466: \newblock \BBOQ Decidability issues for action guarded logics\BBCQ\
467: \newblock In Baader, F.\BBACOMMA\ \BBA\ Sattler, U.\BEDS, {\Bem Proceedings of
468: the 2000 International Workshop on Description Logics {(DL2000)}},
469: \lowercase{\BVOL}~33 of {\Bem CEUR Workshop Proceedings}, \BPGS\ 123--131\
470: RWTH Aachen, Germany.
471: \newblock Available online from
472: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-33/}.
473:
474: \bibitem[\protect\BCAY{Gor{\'e}}{Gor{\'e}}{1998}]{Gore-Tableau-Handbook-1998}
475: Gor{\'e}, R. \BBOP1998\BBCP.
476: \newblock \BBOQ Tableau methods for modal and temporal logics\BBCQ\
477: \newblock In D'Agostino, M., Gabbay, D.~M., H{\"a}hnle, R., \BBA\ Posegga,
478: J.\BEDS, {\Bem Handbook of Tableau Methods}. Kluwer, Dordrecht.
479:
480: \bibitem[\protect\BCAY{Gr{\"a}del}{Gr{\"a}del}{1999a}]{Graedel99b}
481: Gr{\"a}del, E. \BBOP1999a\BBCP.
482: \newblock \BBOQ Decision procedures for guarded logics\BBCQ\
483: \newblock In Ganzinger, H.\BED, {\Bem Automated Deduction - {(CADE-16)}, 16th
484: International Conference on Automated Deduction}, \lowercase{\BNUM}\ 1632 in
485: Lecture Notes in Artificial Intelligence, \BPGS\ 31--51\ Trento, Italy.
486: Springer Verlag.
487:
488: \bibitem[\protect\BCAY{Gr{\"a}del}{Gr{\"a}del}{1999b}]{Graedel99a}
489: Gr{\"a}del, E. \BBOP1999b\BBCP.
490: \newblock \BBOQ On the restraining power of guards\BBCQ\
491: \newblock {\Bem Journal of Symbolic Logic}, {\Bem 64\/}(4), 1719--1742.
492:
493: \bibitem[\protect\BCAY{Gr{\"a}del}{Gr{\"a}del}{1999c}]{Graedel99c}
494: Gr{\"a}del, E. \BBOP1999c\BBCP.
495: \newblock \BBOQ Why are modal logics so robustly decidable?\BBCQ\
496: \newblock {\Bem Bulletin of the European Association for Theoretical Computer
497: Science}, {\Bem 68}, 90--103.
498:
499: \bibitem[\protect\BCAY{Gr{\"a}del}{Gr{\"a}del}{2001}]{graedel-tcs-2001}
500: Gr{\"a}del, E. \BBOP2001\BBCP.
501: \newblock \BBOQ Guarded fixpoint logic and the monadic theory of trees\BBCQ\
502: \newblock {\Bem Theoretical Computer Science}.
503: \newblock To appear, available online from
504: \url{http://www-mgi.informatik.rwth-aachen.de/Publications/pub/graedel/Gr-tc%
505: s01.ps}.
506:
507: \bibitem[\protect\BCAY{Gr{\"a}del, Otto, \BBA\ Rosen}{Gr{\"a}del
508: et~al.}{1997}]{GraedelOttRos97}
509: Gr{\"a}del, E., Otto, M., \BBA\ Rosen, E. \BBOP1997\BBCP.
510: \newblock \BBOQ Two-variable logic with counting is decidable\BBCQ\
511: \newblock In {\Bem Proceedings of 12th IEEE Symposium on Logic in Computer
512: Science {(LICS'97)}}, \BPGS\ 306--317\ Warsaw, Poland. {IEEE} Computer
513: Society Press.
514:
515: \bibitem[\protect\BCAY{Gr{\"a}del \BBA\ Walukiewicz}{Gr{\"a}del \BBA\
516: Walukiewicz}{1999}]{GraedelWal99}
517: Gr{\"a}del, E.\BBACOMMA\ \BBA\ Walukiewicz, I. \BBOP1999\BBCP.
518: \newblock \BBOQ Guarded fixed point logic\BBCQ\
519: \newblock In {\Bem Proceedings of 14th IEEE Symposium on Logic in Computer
520: Science {(LICS'99)}}, \BPGS\ 45--54\ Trento, Italy. {IEEE} Computer Society
521: Press.
522:
523: \bibitem[\protect\BCAY{Haarslev \BBA\ M{\"o}ller}{Haarslev \BBA\
524: M{\"o}ller}{1999}]{Haarslev99a}
525: Haarslev, V.\BBACOMMA\ \BBA\ M{\"o}ller, R. \BBOP1999\BBCP.
526: \newblock \BBOQ {RACE} system description\BBCQ\
527: \newblock In Lambrix, P., Borgida, A., Lenzerini, M., M{\"o}ller, R., \BBA\
528: Patel-Schneider, P.\BEDS, {\Bem Proceedings of the 1999 International
529: Workshop on Description Logics {(DL;99)}}, \lowercase{\BVOL}~22 of {\Bem CEUR
530: Workshop Proceedings}, \BPGS\ 130--132\ Linkoeping, Sweden. Link{\"o}ping
531: University.
532: \newblock Available online from
533: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-22/}.
534:
535: \bibitem[\protect\BCAY{Haarslev \BBA\ M{\"o}ller}{Haarslev \BBA\
536: M{\"o}ller}{2000a}]{HaarslevMoeller-KR-2000}
537: Haarslev, V.\BBACOMMA\ \BBA\ M{\"o}ller, R. \BBOP2000a\BBCP.
538: \newblock \BBOQ Expressive {A}box reasoning with number restrictions, role
539: hierarchies, and transitively closed role\BBCQ\
540: \newblock In Cohn, A.~G., Giunchiglia, F., \BBA\ Selman, B.\BEDS, {\Bem
541: Principles of Knowledge Representation and Reasoning, Proceedings of the 7th
542: International Conference {(KR2000)}}, \BPGS\ 273--284\ Breckenridge, CO, USA.
543: Morgan Kaufman Publishers, Inc.
544:
545: \bibitem[\protect\BCAY{Haarslev \BBA\ M{\"o}ller}{Haarslev \BBA\
546: M{\"o}ller}{2000b}]{HaarslevMoeller-DL-2000-HPR}
547: Haarslev, V.\BBACOMMA\ \BBA\ M{\"o}ller, R. \BBOP2000b\BBCP.
548: \newblock \BBOQ High performance reasoning with very large knowledge
549: bases\BBCQ\
550: \newblock In Baader, F.\BBACOMMA\ \BBA\ Sattler, U.\BEDS, {\Bem Proceedings of
551: the 2000 International Workshop on Description Logics {(DL2000)}},
552: \lowercase{\BVOL}~33 of {\Bem CEUR Workshop Proceedings}\ RWTH Aachen,
553: Germany.
554: \newblock Available online from
555: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-33/}.
556:
557: \bibitem[\protect\BCAY{Haarslev \BBA\ M{\"o}ller}{Haarslev \BBA\
558: M{\"o}ller}{2000c}]{HaarslevMoeller-DL-2000-PSEUDO}
559: Haarslev, V.\BBACOMMA\ \BBA\ M{\"o}ller, R. \BBOP2000c\BBCP.
560: \newblock \BBOQ Optimizing {T}box and {A}box reasoning with pseudo models\BBCQ\
561: \newblock In Baader, F.\BBACOMMA\ \BBA\ Sattler, U.\BEDS, {\Bem Proceedings of
562: the 2000 International Workshop on Description Logics {(DL2000)}},
563: \lowercase{\BVOL}~33 of {\Bem CEUR Workshop Proceedings}\ RWTH Aachen,
564: Germany.
565: \newblock Available online from
566: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-33/}.
567:
568: \bibitem[\protect\BCAY{Halpern \BBA\ Moses}{Halpern \BBA\
569: Moses}{1992}]{HalpernMoses92}
570: Halpern, J.~Y.\BBACOMMA\ \BBA\ Moses, Y. \BBOP1992\BBCP.
571: \newblock \BBOQ A guide to completeness and complexity for model logics of
572: knowledge and belief\BBCQ\
573: \newblock {\Bem Artificial Intelligence}, {\Bem 54\/}(3), 319--379.
574:
575: \bibitem[\protect\BCAY{Hanschke}{Hanschke}{1992}]{hanschke92:_specif_role_inte%
576: r_concep_languag}
577: Hanschke, P. \BBOP1992\BBCP.
578: \newblock \BBOQ Specifying role interaction in concept languages\BBCQ\
579: \newblock In Nebel, B., Rich, C., \BBA\ Swartout, W.~R.\BEDS, {\Bem Principles
580: of Knowledge Representation and Reasoning, Proceedings of the 3rd
581: International Conference {(KR'92)}}, \BPGS\ 318--329\ Cambridge,
582: Massachusetts, USA. Morgan Kaufman Publishers, Inc.
583:
584: \bibitem[\protect\BCAY{Hemaspaandra}{Hemaspaandra}{2000}]{hemaspaandra00:_moda%
585: l_satis_is_deter_linear_space}
586: Hemaspaandra, E. \BBOP2000\BBCP.
587: \newblock \BBOQ Modal satisfiability is in deterministic linear space\BBCQ\
588: \newblock In Clote, P.\BBACOMMA\ \BBA\ Schwichtenberg, H.\BEDS, {\Bem
589: Proceedings of the Annual Conference of the European Association for Computer
590: Science Logic {(CSL-2000)}}, \lowercase{\BNUM}\ 1862 in Lecture Notes in
591: Computer Science, \BPGS\ 332--342\ Fischbachau, Germany. Springer Verlag.
592:
593: \bibitem[\protect\BCAY{Hirsch \BBA\ Tobies}{Hirsch \BBA\
594: Tobies}{2000}]{HirschTobies-AIML-2000}
595: Hirsch, C.\BBACOMMA\ \BBA\ Tobies, S. \BBOP2000\BBCP.
596: \newblock \BBOQ A tableau algorithm for the clique guarded fragment\BBCQ\
597: \newblock In F., W., Wansing, H., de~Rijke, M., \BBA\ Zakharyaschev, M.\BEDS,
598: {\Bem Preliminary Proceedings of the Workshop Advances in Modal Logics
599: {(AiML2000)}}\ Leipzig, Germany.
600:
601: \bibitem[\protect\BCAY{Hollunder}{Hollunder}{1996}]{hollunder96:_consis_check_%
602: reduc_satis_concep_termin_system}
603: Hollunder, B. \BBOP1996\BBCP.
604: \newblock \BBOQ Consistency checking reduced to satisfiability of concepts in
605: terminological systems\BBCQ\
606: \newblock {\Bem Annals of Mathematics and Artificial Intelligence}, {\Bem
607: 18\/}(2--4), 133--157.
608:
609: \bibitem[\protect\BCAY{Hollunder \BBA\ Baader}{Hollunder \BBA\
610: Baader}{1991}]{Hollunder91b}
611: Hollunder, B.\BBACOMMA\ \BBA\ Baader, F. \BBOP1991\BBCP.
612: \newblock \BBOQ Qualifying number restrictions in concept languages\BBCQ\
613: \newblock In Allen, J., Fikes, R., \BBA\ Sandewall, E.\BEDS, {\Bem Principles
614: of Knowledge Representation and Reasoning, Proceedings of the 2nd
615: International Conference {(KR'91)}}, \BPGS\ 335--346\ Cambridge,
616: Massachusetts, USA. Morgan Kaufman Publishers, Inc.
617:
618: \bibitem[\protect\BCAY{Hollunder, Nutt, \BBA\ Schmidt-Schau{\ss}}{Hollunder
619: et~al.}{1990}]{hollunder90:_subsum_algor_concep_descr_languag}
620: Hollunder, B., Nutt, W., \BBA\ Schmidt-Schau{\ss}, M. \BBOP1990\BBCP.
621: \newblock \BBOQ Subsumption algorithms fo concept description languages\BBCQ\
622: \newblock In {\Bem Proceedings of the 9th European Conference on Artificial
623: Intelligence {(ECAI'90)}}, \BPGS\ 348--353\ Stockholm, Sweden.
624:
625: \bibitem[\protect\BCAY{Horrocks}{Horrocks}{1997}]{Horrocks97b}
626: Horrocks, I. \BBOP1997\BBCP.
627: \newblock {\Bem Optimising Tableaux Decision Procedures for Description
628: Logics}.
629: \newblock Ph.D.\ thesis, University of Manchester.
630:
631: \bibitem[\protect\BCAY{Horrocks}{Horrocks}{1998}]{Horrocks98c}
632: Horrocks, I. \BBOP1998\BBCP.
633: \newblock \BBOQ Using an expressive description logic: {FaCT} or fiction?\BBCQ\
634: \newblock In Cohn, A.~G., Schubert, L., \BBA\ Shapiro, S.~C.\BEDS, {\Bem
635: Principles of Knowledge Representation and Reasoning, Proceedings of the 6th
636: International Conference {(KR'98)}}, \BPGS\ 636--647\ Trento, Italy. Morgan
637: Kaufman Publishers, Inc.
638:
639: \bibitem[\protect\BCAY{Horrocks}{Horrocks}{1999}]{horrocks99:_fact}
640: Horrocks, I. \BBOP1999\BBCP.
641: \newblock \BBOQ {FaCT} and {iFaCT}\BBCQ\
642: \newblock In Lambrix, P., Borgida, A., Lenzerini, M., M{\"o}ller, R., \BBA\
643: Patel-Schneider, P.\BEDS, {\Bem Proceedings of the 1999 International
644: Workshop on Description Logics {(DL;99)}}, \lowercase{\BVOL}~22 of {\Bem CEUR
645: Workshop Proceedings}, \BPGS\ 133--135\ Linkoeping, Sweden. Link{\"o}ping
646: University.
647: \newblock Available online from
648: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-22/}.
649:
650: \bibitem[\protect\BCAY{Horrocks}{Horrocks}{2000}]{Horrocks-Tableaux-2000}
651: Horrocks, I. \BBOP2000\BBCP.
652: \newblock \BBOQ Benchmark analysis with {FaCT}\BBCQ\
653: \newblock In Dyckhoff, R.\BED, {\Bem Proceedings of the International
654: Conference on Automated Reasoning with Analytic Tableaux and Related Methods
655: {(TABLEAUX 2000)}}, \lowercase{\BNUM}\ 1847 in Lecture Notes in Artificial
656: Intelligence, \BPGS\ 62--66\ St Andrews, Scotland, UK. Springer Verlag.
657:
658: \bibitem[\protect\BCAY{Horrocks \BBA\ Gough}{Horrocks \BBA\
659: Gough}{1997}]{HorrocksGough-DL-1997}
660: Horrocks, I.\BBACOMMA\ \BBA\ Gough, G. \BBOP1997\BBCP.
661: \newblock \BBOQ Description logics with transitive roles\BBCQ\
662: \newblock In Brachman, R.~J., Donini, F.~M., Franconi, E., Horrocks, I., Levy,
663: A.~Y., \BBA\ Rousset, M.-C.\BEDS, {\Bem Proceedings of the 1996 International
664: Workshop on Description Logics {(DL'97)}}, \BPGS\ 25--28. Universit{\'e}
665: Paris-Sud, Centre d'Orsay, Laboratoire de Recherche en Informatique LRI.
666: \newblock Available online from \url{http://www.lri.fr/~mcr/ps/dl97.html}.
667:
668: \bibitem[\protect\BCAY{Horrocks \BBA\ Patel-Schneider}{Horrocks \BBA\
669: Patel-Schneider}{1999}]{horrocks99:_optim_descr_logic_subsum}
670: Horrocks, I.\BBACOMMA\ \BBA\ Patel-Schneider, P.~F. \BBOP1999\BBCP.
671: \newblock \BBOQ Optimising description logic subsumption\BBCQ\
672: \newblock {\Bem Journal for Logic and Computation}, {\Bem 9\/}(3), 267--293.
673:
674: \bibitem[\protect\BCAY{Horrocks, Patel-Schneider, \BBA\ Sebastiani}{Horrocks
675: et~al.}{2000}]{HorrocksPatelSSebastiani-IGPL-2000}
676: Horrocks, I., Patel-Schneider, P.~F., \BBA\ Sebastiani, R. \BBOP2000\BBCP.
677: \newblock \BBOQ An analysis of empirical testing for modal decision
678: procedures\BBCQ\
679: \newblock {\Bem Logic Journal of the IGPL}, {\Bem 8\/}(3), 293--323.
680:
681: \bibitem[\protect\BCAY{Horrocks \BBA\ Sattler}{Horrocks \BBA\
682: Sattler}{1998}]{HorrocksSattler-DL-1998}
683: Horrocks, I.\BBACOMMA\ \BBA\ Sattler, U. \BBOP1998\BBCP.
684: \newblock \BBOQ A description logic with transitive and converse roles and role
685: hierarchies\BBCQ\
686: \newblock In Franconi, E., Giacomo, G.~D., MacGregor, R.~M., Nutt, W., \BBA\
687: Welty, C.~A.\BEDS, {\Bem Proceedings of the 1998 International Workshop on
688: Description Logics {(DL'98)}}, \lowercase{\BVOL}~11 of {\Bem CEUR Workshop
689: Proceedings}\ IRST, Trento, Italy.
690: \newblock Available online from
691: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-11/}.
692:
693: \bibitem[\protect\BCAY{Horrocks \BBA\ Sattler}{Horrocks \BBA\
694: Sattler}{1999}]{HorrSat-JLC-99}
695: Horrocks, I.\BBACOMMA\ \BBA\ Sattler, U. \BBOP1999\BBCP.
696: \newblock \BBOQ A description logic with transitive and inverse roles and role
697: hierarchies\BBCQ\
698: \newblock {\Bem Journal for Logic and Computation}, {\Bem 9\/}(3), 385--410.
699:
700: \bibitem[\protect\BCAY{Horrocks \BBA\ Sattler}{Horrocks \BBA\
701: Sattler}{2001}]{horrocks01:_ontol_reason_seman_web}
702: Horrocks, I.\BBACOMMA\ \BBA\ Sattler, U. \BBOP2001\BBCP.
703: \newblock \BBOQ Ontology reasoning in the {SHOQ(D)} description logic\BBCQ\
704: \newblock In {\Bem Proceedings of the 17th International Joint Conference on
705: Artificial Intelligence {(IJCAI 2001)}}\ Seattle, USA. Morgan Kaufman
706: Publishers, Inc.
707:
708: \bibitem[\protect\BCAY{Horrocks, Sattler, Tessaris, \BBA\ Tobies}{Horrocks
709: et~al.}{2000}]{HorrocksSattler+-LPAR-2000}
710: Horrocks, I., Sattler, U., Tessaris, S., \BBA\ Tobies, S. \BBOP2000\BBCP.
711: \newblock \BBOQ How to decide query containment under constraints using a
712: description logic\BBCQ\
713: \newblock In Voronkov, A.\BED, {\Bem Logic for Programming and Automated
714: Reasoning, 7th International Conference {(LPAR2000)}}, Lecture Notes in
715: Artificial Intelligence, \BPGS\ 308--325. Springer Verlag.
716:
717: \bibitem[\protect\BCAY{Horrocks, Sattler, \BBA\ Tobies}{Horrocks
718: et~al.}{1999}]{HorrocksSattlerTobies-LPAR-99}
719: Horrocks, I., Sattler, U., \BBA\ Tobies, S. \BBOP1999\BBCP.
720: \newblock \BBOQ Practical reasoning for expressive description logics\BBCQ\
721: \newblock In Ganzinger, H., McAllester, D., \BBA\ Voronkov, A.\BEDS, {\Bem
722: Logic for Programming and Automated Reasoning, 6th International Conference
723: {(LPAR'99)}}, \lowercase{\BNUM}\ 1705 in Lecture Notes in Artificial
724: Intelligence, \BPGS\ 161--180\ Tbilisi, Georgia. Springer Verlag.
725:
726: \bibitem[\protect\BCAY{Horrocks, Sattler, \BBA\ Tobies}{Horrocks
727: et~al.}{2000a}]{HorrSattTob-IGPL}
728: Horrocks, I., Sattler, U., \BBA\ Tobies, S. \BBOP2000a\BBCP.
729: \newblock \BBOQ Practical reasoning for very expressive description
730: logics\BBCQ\
731: \newblock {\Bem Logic Journal of the IGPL}, {\Bem 8\/}(3), 239--264.
732:
733: \bibitem[\protect\BCAY{Horrocks, Sattler, \BBA\ Tobies}{Horrocks
734: et~al.}{2000b}]{HorrSattTob-CADE-2000}
735: Horrocks, I., Sattler, U., \BBA\ Tobies, S. \BBOP2000b\BBCP.
736: \newblock \BBOQ Reasoning with individuals for the description logic
737: {SHIQ}\BBCQ\
738: \newblock In McAllester, D.\BED, {\Bem Automated Deduction - {(CADE-17)}, 17th
739: International Conference on Automated Deduction}, \lowercase{\BNUM}\ 1831 in
740: Lecture Notes in Artificial Intelligence, \BPGS\ 482--496\ Pittsburgh, PA,
741: USA. Springer Verlag.
742:
743: \bibitem[\protect\BCAY{Horrocks \BBA\ Tobies}{Horrocks \BBA\
744: Tobies}{2000}]{HorrocksTobies-KR-2000}
745: Horrocks, I.\BBACOMMA\ \BBA\ Tobies, S. \BBOP2000\BBCP.
746: \newblock \BBOQ Reasoning with axioms: Theory and practice\BBCQ\
747: \newblock In Cohn, A.~G., Giunchiglia, F., \BBA\ Selman, B.\BEDS, {\Bem
748: Principles of Knowledge Representation and Reasoning, Proceedings of the 7th
749: International Conference {(KR2000)}}, \BPGS\ 285--296\ Breckenridge, CO, USA.
750: Morgan Kaufman Publishers, Inc.
751:
752: \bibitem[\protect\BCAY{Ladner}{Ladner}{1977}]{Lad77}
753: Ladner, R.~E. \BBOP1977\BBCP.
754: \newblock \BBOQ The computational complexity of provability in systems of modal
755: propositional logic\BBCQ\
756: \newblock {\Bem SIAM Journal of Computing}, {\Bem 6\/}(3), 467--480.
757:
758: \bibitem[\protect\BCAY{Levesque \BBA\ Brachman}{Levesque \BBA\
759: Brachman}{1987}]{levesque87:_expres_tract_knowl_repres_reason}
760: Levesque, H.~J.\BBACOMMA\ \BBA\ Brachman, R.~J. \BBOP1987\BBCP.
761: \newblock \BBOQ Expressiveness and tractability in knowledge representation and
762: reasoning\BBCQ\
763: \newblock {\Bem Computational Intelligence}, {\Bem 3}, 78--93.
764:
765: \bibitem[\protect\BCAY{Lutz \BBA\ Sattler}{Lutz \BBA\
766: Sattler}{2000}]{LutzSattlerAIML00}
767: Lutz, C.\BBACOMMA\ \BBA\ Sattler, U. \BBOP2000\BBCP.
768: \newblock \BBOQ The complexity of reasoning with boolean modal logic\BBCQ\
769: \newblock In F., W., Wansing, H., de~Rijke, M., \BBA\ Zakharyaschev, M.\BEDS,
770: {\Bem Preliminary Proceedings of the Workshop Advances in Modal Logics
771: {(AiML2000)}}\ Leipzig, Germany.
772:
773: \bibitem[\protect\BCAY{Lutz, Sattler, \BBA\ Tobies}{Lutz
774: et~al.}{1999}]{LutzSattlerTobies-DL-99}
775: Lutz, C., Sattler, U., \BBA\ Tobies, S. \BBOP1999\BBCP.
776: \newblock \BBOQ A suggestion for an $n$-ary description logic\BBCQ\
777: \newblock In Lambrix, P., Borgida, A., Lenzerini, M., M{\"o}ller, R., \BBA\
778: Patel-Schneider, P.\BEDS, {\Bem Proceedings of the 1999 International
779: Workshop on Description Logics {(DL;99)}}, \lowercase{\BVOL}~22 of {\Bem CEUR
780: Workshop Proceedings}\ Linkoeping, Sweden. Link{\"o}ping University.
781: \newblock Available online from
782: \url{http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-22/}.
783:
784: \bibitem[\protect\BCAY{Lutz}{Lutz}{1999}]{Lutz-99d}
785: Lutz, C. \BBOP1999\BBCP.
786: \newblock \BBOQ Complexity of terminological reasoning revisited\BBCQ\
787: \newblock In Ganzinger, H., McAllester, D., \BBA\ Voronkov, A.\BEDS, {\Bem
788: Logic for Programming and Automated Reasoning, 6th International Conference
789: {(LPAR'99)}}, \lowercase{\BNUM}\ 1705 in Lecture Notes in Artificial
790: Intelligence, \BPGS\ 181--200\ Tbilisi, Georgia. Springer Verlag.
791:
792: \bibitem[\protect\BCAY{MacGregor}{MacGregor}{1991}]{macgregor-91a}
793: MacGregor, R. \BBOP1991\BBCP.
794: \newblock \BBOQ Inside the {LOOM} description classifier\BBCQ\
795: \newblock {\Bem ACM SIGART Bulletin}, {\Bem 2\/}(3), 88--92.
796:
797: \bibitem[\protect\BCAY{Marx, Schlobach, \BBA\ Mikul{\'a}s}{Marx
798: et~al.}{2000}]{marx00:_label_deduc_guard_fragm}
799: Marx, M., Schlobach, S., \BBA\ Mikul{\'a}s, S. \BBOP2000\BBCP.
800: \newblock \BBOQ Labelled deduction for the guarded fragment\BBCQ\
801: \newblock In Basin, D., D'Agostino, M., Gabbay, D.~M., Matthews, S., \BBA\
802: Vigan{\`o}, L.\BEDS, {\Bem Labelled Deduction}. Kluwer Academic Publishers,
803: Dordrecht.
804:
805: \bibitem[\protect\BCAY{Massacci}{Massacci}{1999}]{Massacci-Tableaux-1999}
806: Massacci, F. \BBOP1999\BBCP.
807: \newblock \BBOQ Design and results of the {TABLEAUX-99} non-classical (modal)
808: systems comparison\BBCQ\
809: \newblock In Murray, N.\BED, {\Bem Proceedings of the International Conference
810: on Automated Reasoning with Analytic Tableaux and Related Methods
811: {(TABLEAUX'99)}}, \lowercase{\BNUM}\ 1617 in Lecture Notes in Artificial
812: Intelligence\ Saratoga Springs, NY, USA. Springer Verlag.
813:
814: \bibitem[\protect\BCAY{Massacci \BBA\ Donini}{Massacci \BBA\
815: Donini}{2000}]{MassacciDonini-Tableaux2000}
816: Massacci, F.\BBACOMMA\ \BBA\ Donini, F.~M. \BBOP2000\BBCP.
817: \newblock \BBOQ Design and results of {TANCS-2000} non-classical (modal) system
818: comparison\BBCQ\
819: \newblock In Dyckhoff, R.\BED, {\Bem Proceedings of the International
820: Conference on Automated Reasoning with Analytic Tableaux and Related Methods
821: {(TABLEAUX 2000)}}, \lowercase{\BNUM}\ 1847 in Lecture Notes in Artificial
822: Intelligence, \BPGS\ 52--56\ St Andrews, Scotland, UK. Springer Verlag.
823:
824: \bibitem[\protect\BCAY{Mays, Dionne, \BBA\ Weida}{Mays
825: et~al.}{1991}]{mays-etal:1991a}
826: Mays, E., Dionne, R., \BBA\ Weida, R. \BBOP1991\BBCP.
827: \newblock \BBOQ \textsc{k-rep} system overview\BBCQ\
828: \newblock {\Bem ACM SIGART Bulletin}, {\Bem 2\/}(3).
829:
830: \bibitem[\protect\BCAY{McGuinness \BBA\ Wright}{McGuinness \BBA\
831: Wright}{1998}]{mcguinness98:_concep}
832: McGuinness, D.\BBACOMMA\ \BBA\ Wright, J. \BBOP1998\BBCP.
833: \newblock \BBOQ Conceptual modelling for configuration: A description
834: logic-based approach\BBCQ\
835: \newblock {\Bem Artificial Intelligence for Engineering Design, Analysis, and
836: Manufacturing Journal}, {\Bem 12}, 333--344.
837:
838: \bibitem[\protect\BCAY{Minsky}{Minsky}{1981}]{minsky81:_framew_repres_knowl}
839: Minsky, M. \BBOP1981\BBCP.
840: \newblock \BBOQ A framework for representing knowledge\BBCQ\
841: \newblock In Haugeland, J.\BED, {\Bem Mind Design}. The MIT Press.
842: \newblock Republished in \cite{brachman85:_readin_knowl_repres}.
843:
844: \bibitem[\protect\BCAY{Nebel}{Nebel}{1990a}]{nebel90:_reason_revis_hybrid_repr%
845: es_system}
846: Nebel, B. \BBOP1990a\BBCP.
847: \newblock {\Bem Reasoning and Revision in Hybrid Representation Systems}.
848: \newblock \BNUM\ 422 in Lecture Notes in Artificial Intelligence. Springer
849: Verlag, Berlin, Germany.
850:
851: \bibitem[\protect\BCAY{Nebel}{Nebel}{1990b}]{Nebel90}
852: Nebel, B. \BBOP1990b\BBCP.
853: \newblock \BBOQ Terminological reasoning is inherently intractable\BBCQ\
854: \newblock {\Bem Artificial Intelligence}, {\Bem 43\/}(2), 235--249.
855:
856: \bibitem[\protect\BCAY{Nebel}{Nebel}{1988}]{Nebel88}
857: Nebel, B. \BBOP1988\BBCP.
858: \newblock \BBOQ Computational complexity of terminological reasoning in
859: {BACK}\BBCQ\
860: \newblock {\Bem Artificial Intelligence}, {\Bem 34\/}(3), 371--383.
861:
862: \bibitem[\protect\BCAY{Pacholski, Szwast, \BBA\ Tendera}{Pacholski
863: et~al.}{1997}]{LICS::PacholskiST1997}
864: Pacholski, L., Szwast, W., \BBA\ Tendera, L. \BBOP1997\BBCP.
865: \newblock \BBOQ Complexity of two-variable logic with counting\BBCQ\
866: \newblock In {\Bem Proceedings of 12th IEEE Symposium on Logic in Computer
867: Science {(LICS'97)}}, \BPGS\ 318--327\ Warsaw, Poland. {IEEE} Computer
868: Society Press.
869:
870: \bibitem[\protect\BCAY{Papadimitriou}{Papadimitriou}{1994}]{papadimitriou94:_c%
871: ompuat_compl}
872: Papadimitriou, C.~H. \BBOP1994\BBCP.
873: \newblock {\Bem Computational Complexity}.
874: \newblock Addison Wesley Publishing Company.
875:
876: \bibitem[\protect\BCAY{Patel-Schneider}{Patel-Schneider}{2000}]{Patel-Schneide%
877: r-Tableaux2000}
878: Patel-Schneider, P.~F. \BBOP2000\BBCP.
879: \newblock \BBOQ {TANCS-2000} results for {DLP}\BBCQ\
880: \newblock In Dyckhoff, R.\BED, {\Bem Proceedings of the International
881: Conference on Automated Reasoning with Analytic Tableaux and Related Methods
882: {(TABLEAUX 2000)}}, \lowercase{\BNUM}\ 1847 in Lecture Notes in Artificial
883: Intelligence, \BPGS\ 72--76\ St Andrews, Scotland, UK. Springer Verlag.
884:
885: \bibitem[\protect\BCAY{Patel-Schneider, McGuiness, Brachman, Resnick, \BBA\
886: Borgida}{Patel-Schneider et~al.}{1991}]{patel-schneider91:_classic_kr_system}
887: Patel-Schneider, P.~F., McGuiness, D.~L., Brachman, R.~J., Resnick, L.~A.,
888: \BBA\ Borgida, A. \BBOP1991\BBCP.
889: \newblock \BBOQ The \textsc{classic} knowledge representation system: Guiding
890: principles and implementation rational\BBCQ\
891: \newblock {\Bem ACM SIGART Bulletin}, {\Bem 2\/}(3), 108--113.
892:
893: \bibitem[\protect\BCAY{Pratt}{Pratt}{1979}]{Pratt1979}
894: Pratt, V.~R. \BBOP1979\BBCP.
895: \newblock \BBOQ Models of program logics\BBCQ\
896: \newblock In {\Bem 20th Annual Symposium on Foundations of Computer Science},
897: \BPGS\ 115--122\ San Juan, Puerto Rico. {IEEE} Computer Society Press.
898:
899: \bibitem[\protect\BCAY{Quantz \BBA\ Kindermann}{Quantz \BBA\
900: Kindermann}{1990}]{TUB-FB13//TUB-FB13-KIT-78}
901: Quantz, J.\BBACOMMA\ \BBA\ Kindermann, C. \BBOP1990\BBCP.
902: \newblock \BBOQ Implementation of the {BACK}-system version 4\BBCQ\
903: \newblock Technical report\ TUB-FB13-KIT-78, Technical University of Berlin.
904:
905: \bibitem[\protect\BCAY{Quillian}{Quillian}{1967}]{quillian67:_word_concep}
906: Quillian, M.~R. \BBOP1967\BBCP.
907: \newblock \BBOQ Word concepts: A theory and simulation of some basic
908: capabilities\BBCQ\
909: \newblock {\Bem Behavioral Science}, {\Bem 12}, 410--430.
910: \newblock Republished in \cite{brachman85:_readin_knowl_repres}.
911:
912: \bibitem[\protect\BCAY{Rabin}{Rabin}{1969}]{rabin69:_decid_secon_order_theor_a%
913: utom_infin_trees}
914: Rabin, M. \BBOP1969\BBCP.
915: \newblock \BBOQ Decidability of second-order theories and automata on infinite
916: trees\BBCQ\
917: \newblock {\Bem Transactions of the {AMS}}, {\Bem 141}, 1--35.
918:
919: \bibitem[\protect\BCAY{Rector \BBA\ Horrocks}{Rector \BBA\
920: Horrocks}{1997}]{rector:_exper_build_large_re_medic}
921: Rector, A.\BBACOMMA\ \BBA\ Horrocks, I. \BBOP1997\BBCP.
922: \newblock \BBOQ Experience building a large, re-usable medical ontology using a
923: description logic with transitivity and concept inclusions\BBCQ\
924: \newblock In {\Bem Proceedings of the Workshop on Ontological Engineering, AAAI
925: Spring Symposium (AAAI'97)}. AAAI Press, Menlo Park, California.
926:
927: \bibitem[\protect\BCAY{Sattler}{Sattler}{1996a}]{Sattler-KI-1996}
928: Sattler, U. \BBOP1996a\BBCP.
929: \newblock \BBOQ A concept language extended with different kinds of transitive
930: roles\BBCQ\
931: \newblock In G{\"o}rz, G.\BBACOMMA\ \BBA\ H{\"o}lldobler, S.\BEDS, {\Bem
932: {KI-96}: Advances in Artificial Intelligence, 20th Annual German Conference
933: on Artificial Intelligence}, \lowercase{\BNUM}\ 1137 in Lecture Notes in
934: Artificial Intelligence. Springer Verlag.
935:
936: \bibitem[\protect\BCAY{Sattler}{Sattler}{1996b}]{sattler96:_know_repr_in_proc_%
937: engineering}
938: Sattler, U. \BBOP1996b\BBCP.
939: \newblock \BBOQ Knowledge representation in process engineering\BBCQ\
940: \newblock In {\Bem Proceedings of WRKP'96}. DFKI GmbH.
941:
942: \bibitem[\protect\BCAY{Sattler}{Sattler}{1998}]{Sattler-Diss-1998}
943: Sattler, U. \BBOP1998\BBCP.
944: \newblock {\Bem Terminological knowledge representation systems in a process
945: engineering application}.
946: \newblock Aachener {B}erichte zur {I}nformatik, RWTH Aachen.
947:
948: \bibitem[\protect\BCAY{Sattler}{Sattler}{2000}]{Sattler-ECAI-2000}
949: Sattler, U. \BBOP2000\BBCP.
950: \newblock \BBOQ Description logics for the representation of aggregated
951: objects\BBCQ\
952: \newblock In Horn, W.\BED, {\Bem Proceedings of the 14th European Conference on
953: Artificial Intelligence {(ECAI2000)}}, \BPGS\ 239--243\ Berlin, Germany. IOS
954: Press Amsterdam.
955:
956: \bibitem[\protect\BCAY{Savitch}{Savitch}{1970}]{Savitch}
957: Savitch, W.~J. \BBOP1970\BBCP.
958: \newblock \BBOQ Relationship between nondeterministic and deterministic tape
959: complexities\BBCQ\
960: \newblock {\Bem Journal of Computer and System Sciences}, {\Bem 4}, 177--192.
961:
962: \bibitem[\protect\BCAY{Schaerf}{Schaerf}{1994}]{schaerf94:_reason_indiv_concep%
963: _languag}
964: Schaerf, A. \BBOP1994\BBCP.
965: \newblock \BBOQ Reasoning with individuals in concept languages\BBCQ\
966: \newblock {\Bem Data and Knowledge Engineering}, {\Bem 13\/}(2), 141--176.
967:
968: \bibitem[\protect\BCAY{Schild}{Schild}{1991}]{Schi91}
969: Schild, K. \BBOP1991\BBCP.
970: \newblock \BBOQ A correspondence theory for terminological logics: Preliminary
971: report\BBCQ\
972: \newblock In J.~Mylopoulos, R.~R.\BED, {\Bem Proceedings of the 12th
973: International Joint Conference on Artificial Intelligence {(IJCAI-91)}},
974: \BPGS\ 466--471\ Sydney, Australia. Morgan Kaufman Publishers, Inc.
975:
976: \bibitem[\protect\BCAY{Schild}{Schild}{1994}]{Schi94}
977: Schild, K. \BBOP1994\BBCP.
978: \newblock \BBOQ Terminological cycles and the propositional
979: $\mu$-calculus\BBCQ\
980: \newblock In Doyle, J., Sandewall, E., \BBA\ Torasso, P.\BEDS, {\Bem Principles
981: of Knowledge Representation and Reasoning, Proceedings of the 4th
982: International Conference {(KR'94)}}, \BPGS\ 509--520\ Bonn, Germany. Morgan
983: Kaufman Publishers, Inc.
984:
985: \bibitem[\protect\BCAY{Schmidt}{Schmidt}{1998}]{Schmidt98f}
986: Schmidt, R.~A. \BBOP1998\BBCP.
987: \newblock \BBOQ Resolution is a decision procedure for many propositional modal
988: logics\BBCQ\
989: \newblock In Kracht, M., de~Rijke, M., Wansing, H., \BBA\ Zakharyaschev,
990: M.\BEDS, {\Bem Advances in Modal Logic, Volume 1}, \lowercase{\BVOL}~87 of
991: {\Bem Lecture Notes}, \BPGS\ 189--208. CSLI Publications, Stanford.
992:
993: \bibitem[\protect\BCAY{Schmidt-Schau{\ss}}{Schmidt-Schau{\ss}}{1989}]{schmidt-%
994: schausss89:_subsum_klone_undec}
995: Schmidt-Schau{\ss}, M. \BBOP1989\BBCP.
996: \newblock \BBOQ Subsumption in \textsc{kl-one} is undecidable\BBCQ\
997: \newblock In Brachman, R.~J., Levesque, H.~J., \BBA\ Reiter, R.\BEDS, {\Bem
998: Principles of Knowledge Representation and Reasoning, Proceedings of the 1st
999: International Conference {(KR'89)}}, \BPGS\ 421--431\ Toronto, Canada. Morgan
1000: Kaufman Publishers, Inc.
1001:
1002: \bibitem[\protect\BCAY{Schmidt-Schau{\ss} \BBA\ Smolka}{Schmidt-Schau{\ss}
1003: \BBA\ Smolka}{1991}]{Schmidt-Schauss91}
1004: Schmidt-Schau{\ss}, M.\BBACOMMA\ \BBA\ Smolka, G. \BBOP1991\BBCP.
1005: \newblock \BBOQ Attributive concept descriptions with complements\BBCQ\
1006: \newblock {\Bem Artificial Intelligence}, {\Bem 48}, 1--26.
1007:
1008: \bibitem[\protect\BCAY{Schulz \BBA\ Hahn}{Schulz \BBA\
1009: Hahn}{2000}]{schulz:_knowl_engin_large_scale_knowl_reuse}
1010: Schulz, S.\BBACOMMA\ \BBA\ Hahn, U. \BBOP2000\BBCP.
1011: \newblock \BBOQ Knowledge engineering by large-scale knowledge
1012: reuse---experience from the medical domain\BBCQ\
1013: \newblock In Cohn, A.~G., Giunchiglia, F., \BBA\ Selman, B.\BEDS, {\Bem
1014: Principles of Knowledge Representation and Reasoning, Proceedings of the 7th
1015: International Conference {(KR2000)}}, \BPGS\ 601--610\ Breckenridge, CO, USA.
1016: Morgan Kaufman Publishers, Inc.
1017:
1018: \bibitem[\protect\BCAY{Spaan}{Spaan}{1993a}]{Spaan93a}
1019: Spaan, E. \BBOP1993a\BBCP.
1020: \newblock {\Bem Complexity of Modal Logics}.
1021: \newblock Ph.D.\ thesis, Universiteit van Amsterdam.
1022:
1023: \bibitem[\protect\BCAY{Spaan}{Spaan}{1993b}]{spaan_e:1993a}
1024: Spaan, E. \BBOP1993b\BBCP.
1025: \newblock \BBOQ The complexity of propositional tense logics\BBCQ\
1026: \newblock In de~Rijke, M.\BED, {\Bem Diamonds and Defaults}, \BPGS\ 287--307.
1027: Kluwer Academic Publishers, Dordrecht.
1028:
1029: \bibitem[\protect\BCAY{Stockmeyer \BBA\ Meyer}{Stockmeyer \BBA\
1030: Meyer}{1973}]{Stockmeyer-Meyer-73}
1031: Stockmeyer, L.~J.\BBACOMMA\ \BBA\ Meyer, A.~R. \BBOP1973\BBCP.
1032: \newblock \BBOQ Word problems requiring exponential time\BBCQ\
1033: \newblock In {\Bem {ACM} Symposium on Theory of Computing ({STOC} '73)}, \BPGS\
1034: 1--9\ New York. ACM Press.
1035:
1036: \bibitem[\protect\BCAY{Thomas}{Thomas}{1992}]{ThomasHTCS92}
1037: Thomas, W. \BBOP1992\BBCP.
1038: \newblock \BBOQ Automata on infinite objects\BBCQ\
1039: \newblock In van Leeuwen, J.\BED, {\Bem Handbook of Theoretical Computer
1040: Science}, \lowercase{\BVOL}~B. Elsevier and MIT Press.
1041:
1042: \bibitem[\protect\BCAY{Tobies}{Tobies}{1999a}]{Tobies-CSL-99}
1043: Tobies, S. \BBOP1999a\BBCP.
1044: \newblock \BBOQ A {NExpTime}-complete description logic strictly contained in
1045: {$C^2$}\BBCQ\
1046: \newblock In Flum, J.\BBACOMMA\ \BBA\ Rodr{\'i}guez-Artalejo, M.\BEDS, {\Bem
1047: Proceedings of the Annual Conference of the European Association for Computer
1048: Science Logic {(CSL-99)}}, \lowercase{\BNUM}\ 1683 in Lecture Notes in
1049: Computer Science, \BPGS\ 292--306\ Madrid, Spain. Springer Verlag.
1050:
1051: \bibitem[\protect\BCAY{Tobies}{Tobies}{1999b}]{Tobies-CADE-99}
1052: Tobies, S. \BBOP1999b\BBCP.
1053: \newblock \BBOQ A {PSpace} algorithm for graded modal logic\BBCQ\
1054: \newblock In Ganzinger, H.\BED, {\Bem Automated Deduction - {(CADE-16)}, 16th
1055: International Conference on Automated Deduction}, \lowercase{\BNUM}\ 1632 in
1056: Lecture Notes in Artificial Intelligence, \BPGS\ 52--66\ Trento, Italy.
1057: Springer Verlag.
1058:
1059: \bibitem[\protect\BCAY{Tobies}{Tobies}{2000}]{Tobies-JAIR-2000}
1060: Tobies, S. \BBOP2000\BBCP.
1061: \newblock \BBOQ The complexity of reasoning with cardinality restrictions and
1062: nominals in expressive description logics\BBCQ\
1063: \newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 12},
1064: 199--217.
1065:
1066: \bibitem[\protect\BCAY{Tobies}{Tobies}{2001}]{Tobies-JLC-2000}
1067: Tobies, S. \BBOP2001\BBCP.
1068: \newblock \BBOQ {PSPACE} reasoning for graded modal logics\BBCQ\
1069: \newblock {\Bem Journal for Logic and Computation}, {\Bem 11\/}(1), 85--106.
1070:
1071: \bibitem[\protect\BCAY{{van~Benthem}}{{van~Benthem}}{1997}]{Benthem97}
1072: {van~Benthem}, J. \BBOP1997\BBCP.
1073: \newblock \BBOQ Dynamic bits and pieces\BBCQ\
1074: \newblock {ILLC} research report, University of Amsterdam.
1075:
1076: \bibitem[\protect\BCAY{van~der Hoek \BBA\ de~Rijke}{van~der Hoek \BBA\
1077: de~Rijke}{1995}]{VanderHoekdeRijke-JLC-1995}
1078: van~der Hoek, W.\BBACOMMA\ \BBA\ de~Rijke, M. \BBOP1995\BBCP.
1079: \newblock \BBOQ Counting objects\BBCQ\
1080: \newblock {\Bem Journal for Logic and Computation}, {\Bem 5\/}(3), 325--345.
1081:
1082: \bibitem[\protect\BCAY{Vardi}{Vardi}{1996}]{Vardi97}
1083: Vardi, M.~Y. \BBOP1996\BBCP.
1084: \newblock \BBOQ Why is modal logic so robustly decidable?\BBCQ\
1085: \newblock In Immerman, N.\BBACOMMA\ \BBA\ Kolaitis, P.\BEDS, {\Bem Descriptive
1086: Complexity and Finite Models: Proceedings of a DIMACS Workshop, January
1087: 14-17, 1996}, \lowercase{\BNUM}~31 in DIMACS Series in Discrete Mathematics
1088: and Theoretical Computer Science, \BPGS\ 149--184. American Mathematical
1089: Society.
1090:
1091: \bibitem[\protect\BCAY{Vardi}{Vardi}{1998}]{vardi98:_reason_about_past_two_way%
1092: _autom}
1093: Vardi, M.~Y. \BBOP1998\BBCP.
1094: \newblock \BBOQ Reasoning about the past with two-way automata\BBCQ\
1095: \newblock In Larsen, K.~G., Skyum, S., \BBA\ Winskel, G.\BEDS, {\Bem Automata,
1096: Languages and Programming {ICALP} 98}, \lowercase{\BVOL}\ 1443 of {\Bem
1097: Lecture Notes in Computer Science}, \BPGS\ 628--641\ Aalborg, Denmark.
1098: Springer Verlag.
1099:
1100: \bibitem[\protect\BCAY{Vardi \BBA\ Wolper}{Vardi \BBA\ Wolper}{1986}]{VaWo86}
1101: Vardi, M.~Y.\BBACOMMA\ \BBA\ Wolper, P. \BBOP1986\BBCP.
1102: \newblock \BBOQ Automata-theoretic techniques for modal logics of
1103: programs\BBCQ\
1104: \newblock {\Bem Journal of Computer and System Sciences}, {\Bem 32}, 183--221.
1105:
1106: \bibitem[\protect\BCAY{Vardi \BBA\ Wolper}{Vardi \BBA\
1107: Wolper}{1994}]{vardi94:_reason_infin_comput}
1108: Vardi, M.\BBACOMMA\ \BBA\ Wolper, P. \BBOP1994\BBCP.
1109: \newblock \BBOQ Reasoning about infinite computations\BBCQ\
1110: \newblock {\Bem Information and Computation}, {\Bem 115}, 1--37.
1111:
1112: \bibitem[\protect\BCAY{Voronkov}{Voronkov}{1999}]{CADE99*383}
1113: Voronkov, A. \BBOP1999\BBCP.
1114: \newblock \BBOQ {KK}: a theorem prover for {K}\BBCQ\
1115: \newblock In Ganzinger, H.\BED, {\Bem Automated Deduction - {(CADE-16)}, 16th
1116: International Conference on Automated Deduction}, \lowercase{\BNUM}\ 1632 in
1117: Lecture Notes in Artificial Intelligence, \BPGS\ 383--387\ Trento, Italy.
1118: Springer Verlag.
1119:
1120: \bibitem[\protect\BCAY{Voronkov}{Voronkov}{2000}]{Voronkov-LICS-2000}
1121: Voronkov, A. \BBOP2000\BBCP.
1122: \newblock \BBOQ How to optimize proof-search in modal logics: A new way of
1123: proving redundancy for sequent calculi\BBCQ\
1124: \newblock In {\Bem Proceedings of 15th IEEE Symposium on Logic in Computer
1125: Science {(LICS2000)}}\ Santa Barbara, USA. {IEEE} Computer Society Press.
1126:
1127: \bibitem[\protect\BCAY{Wache \BBA\ Kamp}{Wache \BBA\
1128: Kamp}{1996}]{wache96:_using_description_logic_for_configuration}
1129: Wache, H.\BBACOMMA\ \BBA\ Kamp, G. \BBOP1996\BBCP.
1130: \newblock \BBOQ Using description logic for configuration problems\BBCQ\
1131: \newblock In {\Bem Proceedings of WRKP'96}. DFKI GmbH.
1132:
1133: \bibitem[\protect\BCAY{Wang}{Wang}{1963}]{wang63:_domin_aea_decis_probl}
1134: Wang, H. \BBOP1963\BBCP.
1135: \newblock \BBOQ Dominoes and the {AEA} case of the {D}ecision {P}roblem\BBCQ\
1136: \newblock {\Bem Bell {S}ystems {T}echnical {J}ournal}, {\Bem 40}, 1--41.
1137:
1138: \bibitem[\protect\BCAY{Woods}{Woods}{1975}]{woods75:_link}
1139: Woods, W. \BBOP1975\BBCP.
1140: \newblock \BBOQ What's in a link: Foundations for semantic networks\BBCQ\
1141: \newblock In Bobrow, D.\BBACOMMA\ \BBA\ Collins, A.\BEDS, {\Bem Representation
1142: and Understanding: Studies in Cognitive Science}, \BPGS\ 35--82. Academic
1143: Press.
1144:
1145: \bibitem[\protect\BCAY{Woods \BBA\ Schmolze}{Woods \BBA\
1146: Schmolze}{1992}]{woods92:_kl_one_famil}
1147: Woods, W.\BBACOMMA\ \BBA\ Schmolze, J. \BBOP1992\BBCP.
1148: \newblock \BBOQ The {KL-ONE} family\BBCQ\
1149: \newblock {\Bem Computers and Mathematics with Applications, Special Issue on
1150: Semantic Networks in Artificial Intelligence, Part 1}, {\Bem 23\/}(2--5),
1151: 133--178.
1152: \newblock Also available as Technical Report TR-20-90, Aiken Computation
1153: Laboratory, Harvard University.
1154:
1155: \end{thebibliography}
1156: