{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,21]],"date-time":"2026-09-21T12:07:45Z","timestamp":1789992465821,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540676973","type":"print"},{"value":"9783540450085","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_4","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T19:43:15Z","timestamp":1167421395000},"page":"52-56","source":"Crossref","is-referenced-by-count":14,"title":["Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison"],"prefix":"10.1007","author":[{"given":"Fabio","family":"Massacci","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Francesco M.","family":"Donini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Balsinger, P., Heuerding, A.: Comparison of theorem provers for modal logics. In: de Swart, H. (ed.) TABLEAUX 1998. LNCS (LNAI), vol.\u00a01397, pp. 25\u201327. Springer, Heidelberg (1998)","DOI":"10.1007\/3-540-69778-0_4"},{"key":"4_CR2","unstructured":"Cadoli, M., Giovanardi, A., Schaerf, M.: An algorithm to evaluate quantified boolean formulae. In: Proc. of AAAI 1998 (1998)"},{"key":"4_CR3","first-page":"191","volume-title":"Foundation of Knowledge Representation","author":"F. Donini","year":"1996","unstructured":"Donini, F., Lenzerini, M., Nardi, D., Schaerf, A.: Reasoning in description logics. In: Foundation of Knowledge Representation, pp. 191\u2013236. CSLI-Publications, Stanford (1996)"},{"key":"4_CR4","first-page":"365","volume-title":"Handbook of Logic in AI and Logic Programming","author":"M. Fitting","year":"1993","unstructured":"Fitting, M.: Basic modal logic. In: Handbook of Logic in AI and Logic Programming, vol.\u00a01, pp. 365\u2013448. Oxford Univ. Press, Oxford (1993)"},{"issue":"3","key":"4_CR5","doi-asserted-by":"crossref","first-page":"218","DOI":"10.1145\/5666.5673","volume":"29","author":"P. Fleming","year":"1986","unstructured":"Fleming, P., Wallace, J.: How not to lie with statistics: the correct way to summarize benchmark results. CACM\u00a029(3), 218\u2013221 (1986)","journal-title":"CACM"},{"key":"4_CR6","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: More evaluation of decision procedures for modal logics. In: Proc. of KR 1998, pp. 626\u2013635 (1998)"},{"key":"4_CR7","first-page":"319","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"Halpern, J.Y., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. AIJ\u00a054, 319\u2013379 (1992)","journal-title":"AIJ"},{"key":"4_CR8","unstructured":"Johnson, D.: A theoretician\u2019s guide to the experimental analysis of algorithms. Invited talk at AAAI 1996 (August 1996), See http:\/\/www.research.att.com\/~dsj"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Johnson, D., Trick, M. (eds.): Cliques, Coloring, Satisfiability: the second DIMACS implementation challenge. Am. Math. Soc. (1996)","DOI":"10.1090\/dimacs\/026"},{"issue":"3","key":"4_CR10","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","unstructured":"Ladner, R.: The computational complexity of provability in systems of modal propositional logic. SIAM JoC\u00a06(3), 467\u2013480 (1977)","journal-title":"SIAM JoC"},{"key":"4_CR11","series-title":"LNAI","volume-title":"Proc. of TABLEAUX 1999","author":"F. Massacci","year":"1999","unstructured":"Massacci, F.: Design and Results of Tableaux 1999 Non-Classical (Modal) System Competition. In: Proc. of TABLEAUX 1999. LNCS (LNAI). Springer, Heidelberg (1999)"},{"key":"4_CR12","unstructured":"McGuinness, D., Patel-Schneider, P.: Usability Issues in Description Logic Systems. In: Proc. of DL 1997, pp. 84\u201388 (1997)"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Orlin, J.: The complexity of dynamic languages and dynamic optimization pro- blems. In: Proc. of STOC 1981, pp. 218\u2013227 (1981)","DOI":"10.1145\/800076.802475"},{"key":"4_CR14","unstructured":"Rintanen, J.: Improvements to the Evaluation of Quantified Boolean Formulae. In: Proc. of IJCAI 1999, pp. 1192\u20131197 (1999)"},{"issue":"1","key":"4_CR15","first-page":"1","volume":"48","author":"M. Schmidt-Schau\u00df","year":"1991","unstructured":"Schmidt-Schau\u00df, M., Smolka, G.: Attributive Concept Descriptions with Complements. AIJ\u00a048(1), 1\u201326 (1991)","journal-title":"AIJ"},{"issue":"1-2","key":"4_CR16","first-page":"17","volume":"81","author":"B. Selman","year":"1996","unstructured":"Selman, B., Mitchell, D., Levesque, H.: Generating hard satisfiability problems. AIJ\u00a081(1-2), 17\u201329 (1996)","journal-title":"AIJ"},{"issue":"1","key":"4_CR17","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1023\/A:1006006930186","volume":"21","author":"C. Suttner","year":"1998","unstructured":"Suttner, C., Sutcliffe, G.: The CADE-14 ATP system competition. JAR\u00a021(1), 99\u2013134 (1998)","journal-title":"JAR"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722086_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:47:04Z","timestamp":1556005624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/10722086_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}