{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:05:43Z","timestamp":1747548343215},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540676973"},{"type":"electronic","value":"9783540450085"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722086_20","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T00:43:15Z","timestamp":1167439395000},"page":"237-251","source":"Crossref","is-referenced-by-count":3,"title":["A Subset-Matching Size-Bounded Cache for Satisfiability in Modal Logics"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"unstructured":"Hollunder, B., Nutt, W., Schmidt-Schau\u00df, M.: Subsumption Algorithms for Concept Description Languages. In: Proc. 8th European Conference on Artificial Intelligence, pp. 348\u2013353 (1990)","key":"20_CR1"},{"key":"20_CR2","first-page":"109","volume":"4","author":"F. Baader","year":"1994","unstructured":"Baader, F., Franconi, E., Hollunder, B., Nebel, B., Profitlich, H.J.: An Empirical Analysis of Optimization Techniques for Terminological Representation Systems or: Making KRIS get a move on. Applied Artificial Intelligence. Special Issue on Knowledge Base Management\u00a04, 109\u2013132 (1994)","journal-title":"Applied Artificial Intelligence. Special Issue on Knowledge Base Management"},{"key":"20_CR3","series-title":"LNAI","volume-title":"Automated Deduction - Cade-13","author":"F. Giunchiglia","year":"1996","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS (LNAI), vol.\u00a01104. Springer, Heidelberg (1996)"},{"unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R., Tacchella, A.: More evaluation of decision procedures for modal logics. In: Sixth International Conference on Principles of Knowledge Representation and Reasoning, KR 1998 (1998)","key":"20_CR4"},{"issue":"1","key":"20_CR5","first-page":"177","volume":"2","author":"A. Heuerding","year":"1996","unstructured":"Heuerding, A., Jager, G., Schwendimann, S., Seyfried, M.: The Logics Workbench LWB: A Snapshot. Euromath Bulletin\u00a02(1), 177\u2013186 (1996)","journal-title":"Euromath Bulletin"},{"unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction? In: Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR 1998), pp. 636\u2013647 (1998)","key":"20_CR6"},{"unstructured":"Tacchella, A.: *sat system description. In: Lambrix, P., Borgida, A., Lenzerini, M., M\u00f6ller, R., Patel-Schneider, P. (eds.) Collected Papers from the International Description Logics Workshop (DL 1999). CEUR (July 999)","key":"20_CR7"},{"doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Giunchiglia, F., Tacchella, A.: SAT-Based Decision Procedures for Classical Modal Logics. Journal of Automated Reasoning (2000) (to appear)","key":"20_CR8","DOI":"10.1007\/3-540-46238-4_9"},{"key":"20_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/3-540-48660-7_35","volume-title":"Automated Deduction - CADE-16","author":"A. Voronkov","year":"1999","unstructured":"Voronkov, A.: KK: a theorem prover for K. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol.\u00a01632, pp. 383\u2013387. Springer, Heidelberg (1999)"},{"unstructured":"Patel-Schneider, P.F.: DLP system description. In: Franconi, E., De Giacomo, G., MacGregor, R.M., Nutt, W., Welty, C.A., Sebastiani, F. (eds.) Collected Papers from the International Description Logics Workshop (DL 1998), CEUR, pp. 87\u201389 (May 1998)","key":"20_CR10"},{"unstructured":"Haarslev, V., Moeller, R.: HAM-ALC. In: Franconi, E., De Giacomo, G., MacGregor, R.M., Nutt, W., Welty, C.A., Sebastiani, F. (eds.) Collected Papers from the International Description Logics Workshop (DL 1998). CEUR (May 1998)","key":"20_CR11"},{"key":"20_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/3-540-48754-9_5","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"V. Boyapati","year":"1999","unstructured":"Boyapati, V., Gor\u00e9, R.: KtSeqC: System description. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 29\u201331. Springer, Heidelberg (1999)"},{"unstructured":"Hustadt, U., Schmidt, R.A., Weidenbach, C.: MSPASS: Subsumption testing with SPASS. In: Lambrix, P., Borgida, A., Lenzerini, M., M\u00f6ller, R., Patel- Schneider, P. (eds.) Collected Papers from the International Description Logics Workshop (DL 1999). CEUR, pp. 136\u2013137 (July 1999)","key":"20_CR13"},{"unstructured":"Massacci, F.: Results of the TANCS comparison (1999), Accessed March 9 (2000), http:\/\/www.dis.uniroma1.it\/~tancs\/results.shtml","key":"20_CR14"},{"unstructured":"Horrocks, I., Patel-Schneider, P.F.: Advances in propositional modal satisfiability (1999) (manuscript)","key":"20_CR15"},{"key":"20_CR16","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511621192","volume-title":"Modal Logic - an Introduction","author":"B.F. Chellas","year":"1980","unstructured":"Chellas, B.F.: Modal Logic - an Introduction. Cambridge University Press, Cambridge (1980)"},{"doi-asserted-by":"crossref","unstructured":"Davis, M., Longemann, G., Loveland, D.: A machine program for theorem proving. Journal of the ACM\u00a05(7) (1962)","key":"20_CR17","DOI":"10.1145\/368273.368557"},{"key":"20_CR18","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A Structure-preserving Clause Form Translation. Journal of Symbolic Computation\u00a02, 293\u2013304 (1986)","journal-title":"Journal of Symbolic Computation"},{"key":"20_CR19","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","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. Artificial Intelligence\u00a054, 319\u2013379 (1992)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"20_CR20","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 J. Comp.\u00a06(3), 467\u2013480 (1977)","journal-title":"SIAM J. Comp."},{"key":"20_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-48754-9_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"F. Massacci","year":"1999","unstructured":"Massacci, F.: Design and results of the Tableaux 1999 Non-classical (Modal) Systems comparison. In: Murray, N.V. (ed.) TABLEAUX 1999. LNCS (LNAI), vol.\u00a01617, pp. 14\u201318. Springer, Heidelberg (1999)"},{"unstructured":"Hoffman, J., Koehler, J.: A new method to index and query sets. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 1999), pp. 462\u2013467 (1999)","key":"20_CR22"},{"key":"20_CR23","series-title":"LNAI","doi-asserted-by":"publisher","DOI":"10.1007\/10722086_9","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"A. Tacchella","year":"2000","unstructured":"Tacchella, A.: Evaluating *sat on TANCS2000 benchmarks. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol.\u00a01847. Springer, Heidelberg (2000)"}],"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_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T11:47:11Z","timestamp":1556020031000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722086_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540676973","9783540450085"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/10722086_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}