Horrocks, I. (1998). Using an expressive description logic: FaCT or fiction?. In Cohn, A. G., Schubert, L., & Shapiro, S. C. (Eds.), *Principles of Knowledge Representation and Reasoning:*
Proceedings of the Sixth International Conference (KR'98), pp. 636–647. Morgan Kaufmann Publishers, San Francisco, California.

Horrocks, I., & Patel-Schneider, P. F. (2002). Evaluating optimised decision procedures for propositional modal K(m) satisfiability. *Journal of Automated Reasoning,* 28(2), 173–204.

Horrocks, I., Patel-Schneider, P. F., & Sebastiani, R. (2000). An analysis of empirical testing for modal decision procedures. *Logic Journal of the IGPL,* 8(3), 293–323.

Hustadt, U., & Schmidt, R. A. (1999). An empirical analysis of modal theorem provers. *Journal of* Applied Non-Classical Logics, 9(4), 479–522.

Hustadt, U., Schmidt, R. A., & Weidenbach, C. (1999). MSPASS: Subsumption testing with SPASS.

In Lambrix, P., Borgida, A., Lenzerini, M., M¨oller, R., & Patel-Schneider, P. (Eds.), *Proceedings of the 1999 International Workshop on Description Logics (DL'99).*, pp. 136–137.

Massacci, F. (1999). Design and results of Tableaux-99 non-classical (modal) system competition.

In *Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'99*, Vol. 1617 of *Lecture Notes in Artificial Intelligence*, pp. 14–18, Berlin.

Springer.

Mitchell, D., Selman, B., & Levesque, H. (1992). Hard and easy distributions of SAT problems.

In *Proceedings of the Tenth National Conference on Artificial Intelligence*, pp. 459–465, San Jose, California. American Association for Artificial Intelligence.

Patel-Schneider, P. F. (1998). DLP system description. In Franconi, E., Giacomo, G. D., MacGregor, R. M., Nutt, W., Welty, C. A., & Sebastiani, F. (Eds.), *Collected Papers from the International Description Logics Workshop (DL'98)*, pp. 87–89. Available as CEUR-WS/Vol-11 from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS.

Patel-Schneider, P. F., & Sebastiani, R. (2001). A new system and methodology for generating random modal formulae. In Proceedings of the International Joint Conference on Automated Reasoning, IJCAR'2001, Vol. 2083 of *Lecture Notes in Computer Science*, pp. 464–468, Siena, Italy. Springer.

Pitt, J., & Cunningham, J. (1996). Distributed modal theorem proving with KE. In Minglioli, P.,
Moscato, U., Mindici, D., & Ornaghi, M. (Eds.), *Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux'96*, Vol. 1071 of Lecture Notes in Artificial Intelligence, pp. 160–176, Berlin. Springer.

Tacchella, A. (1999). *SAT system description. In Lambrix, P., Borgida, A., Lenzerini, M., M¨oller, R., & Patel-Schneider, P. (Eds.), *Proceedings of the 1999 International Workshop on Description Logics (DL'99).*, pp. 142–144.