{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,19]],"date-time":"2025-05-19T04:01:17Z","timestamp":1747627277413,"version":"3.40.5"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,9,1]],"date-time":"2001-09-01T00:00:00Z","timestamp":999302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Annals of Mathematics and Artificial Intelligence"],"published-print":{"date-parts":[[2001,9]]},"DOI":"10.1023\/a:1012380814999","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T18:14:30Z","timestamp":1041185670000},"page":"39-67","source":"Crossref","is-referenced-by-count":3,"title":["A Subset-Matching Size-Bounded Cache for Testing Satisfiability in Modal Logics"],"prefix":"10.1007","volume":"33","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"3-4","key":"359697_CR1","doi-asserted-by":"crossref","first-page":"475","DOI":"10.1007\/BF01530803","volume":"8","author":"A. Armando","year":"1993","unstructured":"A. Armando and E. Giunchiglia, Embedding complex decision procedures inside an interactive theorem prover, Annals of Mathematics and Artificial Intelligence 8(3-4) (1993) 475-502.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"359697_CR2","first-page":"109","volume":"4","author":"F. Baader","year":"1994","unstructured":"F. Baader, E. Franconi, B. Hollunder, B. Nebel, and H.J. Profitlich, 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 4 (1994) 109-132.","journal-title":"Applied Artificial Intelligence. Special Issue on Knowledge Base Management"},{"key":"359697_CR3","series-title":"Lecture Notes in Artificial Intelligence","first-page":"29","volume-title":"Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), 07-11 June 1999","author":"V. Boyapati","year":"1999","unstructured":"V. Boyapati and R. Gor\u00e9, KtSeqC: System description, in: Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), 07-11 June 1999, ed. N.V. Murray, Lecture Notes in Artificial Intelligence, Vol. 1617 (Springer, Berlin, 1999) pp. 29-31."},{"key":"359697_CR4","doi-asserted-by":"crossref","unstructured":"B.F. Chellas, Modal Logic-An Introduction (Cambridge University Press, 1980).","DOI":"10.1017\/CBO9780511621192"},{"key":"359697_CR5","doi-asserted-by":"crossref","unstructured":"M. Davis, G. Longemann, and D. Loveland, A machine program for theorem proving, Journal of the ACM 5(7) (1962).","DOI":"10.1145\/368273.368557"},{"key":"359697_CR6","doi-asserted-by":"crossref","unstructured":"T. Boy de la Tour, Minimizing the number of clauses by renaming, in: Proc. of 10th Conference on Automated Deduction (Springer, 1990) pp. 558-572.","DOI":"10.1007\/3-540-52885-7_114"},{"key":"359697_CR7","unstructured":"I.P. Gent, H. Van Maaren and T. Walsh (eds.), SAT2000. Highlights of Satisfiability Research in the Year 2000 (IOS Press, 2000)."},{"key":"359697_CR8","unstructured":"E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and A. Tacchella, More evaluation of decision procedures for modal logics, in: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR'98) (1998)."},{"issue":"2","key":"359697_CR9","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1080\/11663081.2000.10510994","volume":"10","author":"E. Giunchiglia","year":"2000","unstructured":"E. Giunchiglia, F. Giunchiglia, R. Sebastiani and A. Tacchella, SAT vs. translation based decision procedures for modal logics: a comparative evaluation, Journal of Applied Non Classical Logics 10(2) (2000) 145-172.","journal-title":"Journal of Applied Non Classical Logics"},{"key":"359697_CR10","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia, F. Giunchiglia and A. Tacchella, SAT-based decision procedures for classical modal logics, Journal of Automated Reasoning, 2000, to appear. Reprinted in [7].","DOI":"10.1007\/3-540-46238-4_9"},{"key":"359697_CR11","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia and A. Tacchella, A subset-matchig size-bounded cache for satisfiability in modal logics, in: Proc. of International Conference on Theorem Proving with Analytic Tableaux and Related Methods (Tableaux 2000) (July 2000).","DOI":"10.1007\/10722086_20"},{"key":"359697_CR12","doi-asserted-by":"crossref","unstructured":"E. Giunchiglia and A. Tacchella, *SAT: a system for the development of modal decision procedures, in: Proc. of 17th International Conference on Automated Deduction (CADE'2000) (2000) pp. 291-296.","DOI":"10.1007\/10721959_22"},{"key":"359697_CR13","doi-asserted-by":"crossref","unstructured":"F. Giunchiglia and R. Sebastiani, Building decision procedures for modal logics from propositional decision procedures-the case study of modal K, in: Proc. of CADE-96, New Brunswick, NJ, USA, August 1996, Lecture Notes in Artificial Intelligence (Springer, 1996).","DOI":"10.1007\/3-540-61511-3_115"},{"key":"359697_CR14","first-page":"431","volume-title":"Proc. of 15th National Conference on Artificial Intelligence (AAAI-98) and of 10th Conference on Innovative Applications of Artificial Intelligence (IAAI-98), 26-30 July","author":"C.P. Gomes","year":"1998","unstructured":"C.P. Gomes, B. Selman and H. Kautz, Boosting combinatorial search through randomization. in: Proc. of 15th National Conference on Artificial Intelligence (AAAI-98) and of 10th Conference on Innovative Applications of Artificial Intelligence (IAAI-98), 26-30 July (AAAI Press, Menlo Park, CA, 1998) pp. 431-437."},{"key":"359697_CR15","unstructured":"V. Haarslev and R. M\u00f6ller, HAM-ALC, in: Collected Papers from the International Description Logics Workshop (DL'98), eds. E. Franconi, G. De Giacomo, R.M. MacGregor, W. Nutt, C.A. Welty and F. Sebastiani (CEUR, May 1998)."},{"key":"359697_CR16","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"J.Y. Halpern","year":"1992","unstructured":"J.Y. Halpern and Y. Moses, A guide to completeness and complexity for modal logics of knowledge and belief, Artificial Intelligence 54 (1992) 319-379.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"359697_CR17","first-page":"177","volume":"2","author":"A. Heuerding","year":"1996","unstructured":"A. Heuerding, G. Jager, S. Schwendimann and M. Seyfried, The logics workbench LWB: A snapshot, Euromath Bulletin 2(1) (1996) 177-186.","journal-title":"Euromath Bulletin"},{"key":"359697_CR18","unstructured":"J. Hoffman and J. Koehler, A new method to index and query sets, in: Proc. of 16th International Joint Conference on Artificial Intelligence (IJCAI-99) (1999) pp. 462-467."},{"key":"359697_CR19","unstructured":"B. Hollunder, W. Nutt and M. Schmidt-Schau\u00df, Subsumption algorithms for concept description languages, in: Proc. of 8th European Conference on Artificial Intelligence (1990) pp. 348-353."},{"key":"359697_CR20","unstructured":"I. Horrocks, Using an expressive description logic: FaCT or fiction?, in: Proc. of 6th International Conference on Principles of Knowledge Representation and Reasoning (KR'98) (1998) pp. 636-647."},{"key":"359697_CR21","unstructured":"I. Horrocks and P.F. Patel-Schneider, Advances in propositional modal satisfiability, manuscript (1999)."},{"key":"359697_CR22","unstructured":"U. Hustadt, R.A. Schmidt and C. Weidenbach, MSPASS: Subsumption testing with SPASS. in: Collected Papers from the International Description Logics Workshop (DL'99), eds. P. Lambrix, A. Borgida, M. Lenzerini, R. M\u00f6ller and P. Patel-Schneider (CEUR, July 1999) pp. 136-137."},{"issue":"3","key":"359697_CR23","doi-asserted-by":"crossref","first-page":"467","DOI":"10.1137\/0206033","volume":"6","author":"R. Ladner","year":"1977","unstructured":"R. Ladner, The computational complexity of provability in systems of modal propositional logic, SIAM Journal on Computing 6(3) (1977) 467-480.","journal-title":"SIAM Journal on Computing"},{"key":"359697_CR24","series-title":"Lecture Notes in Artificial Intelligence","first-page":"14","volume-title":"Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), 07-11 June 1999","author":"F. Massacci","year":"1999","unstructured":"F. Massacci, Design and results of the Tableaux-99 non-classical (modal) systems comparison, in: Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-99), 07-11 June 1999, ed. N.V. Murray, Lecture Notes in Artificial Intelligence, Vol. 1617 (Springer, Berlin, 1999) pp. 14-18."},{"key":"359697_CR25","series-title":"Lecture Notes in Artificial Intelligence","first-page":"52","volume-title":"Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-2000), 3-7 July 2000","author":"F. Massacci","year":"2000","unstructured":"F. Massacci and F. Donini, Design and results of TANCS-2000 non-classical (molda) systems comparison, in: Proc. of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-2000), 3-7 July 2000, ed. R. Dyckhoff, Lecture Notes in Artificial Intelligence, Vol. 1847 (Springer, Berlin, 2000) pp. 52-56."},{"key":"359697_CR26","unstructured":"P.F. Patel-Schneider, DLP system description, in: Collected Papers from the International Description Logics Workshop (DL'98), eds. E. Franconi, G. De Giacomo, R.M. MacGregor, W. Nutt, C.A. Welty and F. Sebastiani (CEUR, May 1998) pp. 87-89."},{"key":"359697_CR27","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"D.A. Plaisted and S. Greenbaum, A structure-preserving clause form translation, Journal of Symbolic Computation 2 (1986) 293-304.","journal-title":"Journal of Symbolic Computation"},{"key":"359697_CR28","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1016\/0004-3702(92)90049-4","volume":"54","author":"M. Schmidt-Schauss","year":"1992","unstructured":"M. Schmidt-Schauss and G. Smolka, Attributive concept descriptions with complements. Artificial Intelligence 54 (1992) 319-379.","journal-title":"Artificial Intelligence"},{"key":"359697_CR29","doi-asserted-by":"crossref","unstructured":"J. Siekmann and G. Wrightson (eds.), Automation of Reasoning: Classical Papers in Computational Logic 1967-1970, Vol. 2 (Springer, 1983).","DOI":"10.1007\/978-3-642-81955-1"},{"key":"359697_CR30","unstructured":"A. Tacchella, *SAT system description, in: Collected Papers from the International Description Logics Workshop (DL'99), eds. P. Lambrix, A. Borgida, M. Lenzerini, R. M\u00f6ller and P. Patel-Schneider (CEUR, July 1999)."},{"key":"359697_CR31","doi-asserted-by":"crossref","unstructured":"G. Tseitin, On the complexity of proofs in propositional logics, Seminars in Mathematics 8 (1970). Reprinted in [29].","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"359697_CR32","first-page":"243","volume-title":"Proc. of 4th Annual Symposium on Logic in Computer Science, Asilomar Conference Center, 5-8 June 1989","author":"M.Y. Vardi","year":"1989","unstructured":"M.Y. Vardi, On the complexity of epistemic reasoning. in: Proc. of 4th Annual Symposium on Logic in Computer Science, Asilomar Conference Center, 5-8 June 1989 (IEEE Computer Society Press, Pacific Grove, CA, 1989) pp. 243-252."},{"key":"359697_CR33","series-title":"Lecture Notes in Artificial Intelligence","first-page":"383","volume-title":"Proc. of 16th International Conference on Automated Deduction (CADE-16), 7-10 July 1999","author":"A. Voronkov","year":"1999","unstructured":"A. Voronkov, KK: a theorem prover for K, in: Proc. of 16th International Conference on Automated Deduction (CADE-16), 7-10 July 1999, ed. H. Ganzinger, Lecture Notes in Artificial Intelligence, Vol. 1632 (Springer, Berlin, 1999) pp. 383-387."}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012380814999.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1012380814999\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1012380814999.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T05:47:18Z","timestamp":1747547238000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1012380814999"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,9]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,9]]}},"alternative-id":["359697"],"URL":"https:\/\/doi.org\/10.1023\/a:1012380814999","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2001,9]]}}}