{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T14:31:25Z","timestamp":1761661885617,"version":"3.41.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"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":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1023\/a:1015071400913","type":"journal-article","created":{"date-parts":[[2002,12,28]],"date-time":"2002-12-28T22:07:59Z","timestamp":1041113279000},"page":"143-171","source":"Crossref","is-referenced-by-count":29,"title":["SAT-Based Decision Procedures for Classical Modal Logics"],"prefix":"10.1007","volume":"28","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"395297_CR1","first-page":"109","volume":"4","author":"F. Baader","year":"1994","unstructured":"Baader, F., Franconi, E., Hollunder, B., Nebel, B. and Profitlich, H. J.: An empirical analysis of optimization techniques for terminological representation systems, or Making KRIS get a move on, Appl. Artificial Intelligence. Special Issue on Knowledge Base Management\n4 (1994), 109\u2013132.","journal-title":"Appl. Artificial Intelligence. Special Issue on Knowledge Base Management"},{"key":"395297_CR2","unstructured":"Baker, A.: Intelligent backtracking on the hardest constraint problems, 1995."},{"key":"395297_CR3","unstructured":"Cadoli, M., Giovanardi, A. and Schaerf, M.: An algorithm to evaluate quantified boolean formulae, in Proc. AAAI, 1998."},{"key":"395297_CR4","doi-asserted-by":"crossref","unstructured":"Chellas, B. F.: Modal Logic \u2014 an Introduction, Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"395297_CR5","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"Davis, M. and Putnam, H.: A computing procedure for quantification theory, J. ACM\n7 (1960), 201\u2013215.","journal-title":"J. ACM"},{"key":"395297_CR6","doi-asserted-by":"crossref","unstructured":"Boy de la Tour, T.: Minimizing the number of clauses by renaming, in Proc. of the 10th Conference on Automated Deduction, Springer-Verlag, 1990, pp. 558\u2013572.","DOI":"10.1007\/3-540-52885-7_114"},{"key":"395297_CR7","doi-asserted-by":"crossref","unstructured":"de Swart, H. (ed.): Automated Reasoning with Analytic Tableaux and RelatedMethods: International Conference Tableaux'98, Lecture Notes in Artificial Intelligence 1397, Springer-Verlag, May 1998.","DOI":"10.1007\/3-540-69778-0"},{"key":"395297_CR8","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J. Y., Moses, Y. and Vardi, M. Y.: Reasoning about Knowledge, MIT Press, 1995.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"395297_CR9","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logics, D. Reidel, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"395297_CR10","unstructured":"Franconi, E., De Giacomo, G., MacGregor, R. M., Nutt, W., Welty, C. A. and Sebastiani, F. (eds.): Collected Papers from the International Description Logics Workshop (DL'98), CEUR, May 1998."},{"key":"395297_CR11","unstructured":"Freeman, J. W.: Improvements to propositional satisfiability search algorithms, Ph.D. Thesis, University of Pennsylvania, 1995."},{"key":"395297_CR12","doi-asserted-by":"crossref","unstructured":"Gasquet, O. and Herzig, A.: From classical to normal modal logics, in H. Wansing (ed.), Proof Theory of Modal Logics, Appl. Logic Series 2, Kluwer Academic Publishers, 1996, pp. 293\u2013311.","DOI":"10.1007\/978-94-017-2798-3_15"},{"key":"395297_CR13","series-title":"Technical Report","volume-title":"Proc. International Conference on Formal and Applied Practical Reasoning (FAPR'96)","author":"E. Giunchiglia","year":"1997","unstructured":"Giunchiglia, E. and Giunchiglia, F.: Ideal and real belief about belief, Technical Report 96-0138, DIST, University of Genoa, Italy, September 1997. Also IRST-Technical Report 9605-04. A short version of the paper appeared in the Proc. International Conference on Formal and Applied Practical Reasoning (FAPR'96)."},{"key":"395297_CR14","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F. and Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures \u2014 the case study of modal K, in Proc. CADE-96, Lecture Notes in Artificial Intelligence, Springer-Verlag, New Brunswick, NJ, USA, August 1996.","DOI":"10.1007\/3-540-61511-3_115"},{"key":"395297_CR15","unstructured":"Giunchiglia, F. and Sebastiani, R.: A SAT-based decision procedure for ALC, in Proc. of the 5th International Conference on Principles of Knowledge Representation and Reasoning \u2014 KR'96, Cambridge, MA, USA, November 1996. Also DIST-Technical Report 9607-08 and IRST-Technical Report 9601-02."},{"key":"395297_CR16","unstructured":"Giunchiglia, E., Giunchiglia, F., Sebastiani, R. and Tacchella, A.: More evaluation of decision procedures for modal logics, in Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), 1998."},{"key":"395297_CR17","unstructured":"Governatori, G. and Luppi, A.: Labelled tableaux for non-normal modal logics, in Sixth Conference of the Italian Association for Artificial Intelligence, AI*IA '99, Bologna, Italy, September 14\u201317, 1999."},{"key":"395297_CR18","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Comparing subsumption optimizations, in E. Franconi, G. De Giacomo, R. M. MacGregor, W. Nutt, C. A. Welty, and F. Sebastiani (eds.), Collected Papers from the International Description Logics Workshop (DL'98), CEUR, May 1998, pp. 90\u201394."},{"key":"395297_CR19","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Advances in propositional modal satisfiability, 1999. Manuscript."},{"key":"395297_CR20","doi-asserted-by":"crossref","unstructured":"Horrocks, I. and Patel-Schneider, P. F.: Optimising description logic subsumption, J. Logic Comput. (1999), to appear.","DOI":"10.1093\/logcom\/9.3.267"},{"key":"395297_CR21","unstructured":"Horrocks, I.: Using an expressive description logic: FaCT or fiction?, in Sixth International Conference on Principles of Knowledge Representation and Reasoning (KR'98), 1998, pp. 636\u2013647."},{"key":"395297_CR22","unstructured":"Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logic, in Proc. of the 15th International Joint Conference on Artificial Intelligence, 1997."},{"key":"395297_CR23","series-title":"Research Report","volume-title":"On evaluating decision procedures for modal logic","author":"U. Hustadt","year":"1997","unstructured":"Hustadt, U. and Schmidt, R. A.: On evaluating decision procedures for modal logic, Research Report MPI-I-97-2-003, Max-Planck-Institut f\u00fcr Informatik, Saarbr\u00fccken, Germany, February 1997."},{"key":"395297_CR24","unstructured":"Kautz, H. and Selman, B.: BLACKBOX: A new approach to the application of theorem proving to problem solving, in Working Notes of the Workshop on Planning as Combinatorial Search, held in conjunction with AIPS-98, 1998."},{"key":"395297_CR25","doi-asserted-by":"crossref","unstructured":"Massacci, F.: Strongly analytic tableaux for normal modal logics, in Proc. CADE, 1994.","DOI":"10.1007\/3-540-58156-1_52"},{"key":"395297_CR26","first-page":"102","volume-title":"Contemporary Philosophy: A Survey. I","author":"R. Montague","year":"1968","unstructured":"Montague, R.: Pragmatics, in R. Klibansky (ed.), Contemporary Philosophy: A Survey. I, La Nuova Italia Editrice, Florence, 1968, pp. 102\u2013122. Reprinted in Formal Philosophy, by Richard Montague, Yale University Press, New Haven, CT, 1974, pp. 95\u2013118."},{"key":"395297_CR27","doi-asserted-by":"crossref","unstructured":"Ohlbach, H. J.: Translation methods for non-classical logics \u2014 an overview, Bull. of the Interest Group in Pure and Applied Logic \u2014 IGPL\n1(1) (1988).","DOI":"10.1093\/jigpal\/1.1.69"},{"key":"395297_CR28","unstructured":"Patel-Schneider, P. F.: DLP system description, in E. Franconi, G. De Giacomo, R. M. Mac-Gregor, W. Nutt, C. A. Welty, and F. Sebastiani (eds.), Collected Papers from the International Description Logics Workshop (DL'98), CEUR, May 1998, pp. 87\u201389."},{"key":"395297_CR29","unstructured":"Patel-Schneider, P. F.: Personal communication, June 1999."},{"key":"395297_CR30","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D. A. Plaisted","year":"1986","unstructured":"Plaisted, D. A. and Greenbaum, S.: A structure-preserving clause form translation, J. Symbolic Comput. 2 (1986) 293\u2013304.","journal-title":"J. Symbolic Comput"},{"key":"395297_CR31","series-title":"Technical Report","volume-title":"From tableau-based to SAT-based procedures \u2014 preliminary report","author":"R. Sebastiani","year":"1997","unstructured":"Sebastiani, R. and Giunchiglia, F.: From tableau-based to SAT-based procedures \u2014 preliminary report, Technical Report 9711-14, IRST, Trento, Italy, November 1997."},{"key":"395297_CR32","volume-title":"An Essay in Classical Modal Logic","author":"K. Segerberg","year":"1971","unstructured":"Segerberg, K.: An Essay in Classical Modal Logic, 1st edn, Philosophical Studies, Uppsala, 1971.","edition":"1st edn"},{"key":"395297_CR33","doi-asserted-by":"crossref","unstructured":"Siekmann, J. and Wrightson, G. (eds.): Automation of Reasoning: Classical Papers in Computational Logic 1967\u20131970, Vol. 2, Springer-Verlag, 1983.","DOI":"10.1007\/978-3-642-81955-1"},{"key":"395297_CR34","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R. M. Smullyan","year":"1968","unstructured":"Smullyan, R. M.: First-Order Logic, Springer-Verlag, New York, 1968."},{"key":"395297_CR35","unstructured":"Tacchella, A.: *SAT system description, in Collected Papers from the International Description Logics Workshop (DL'99), CEUR, July 1999."},{"key":"395297_CR36","doi-asserted-by":"crossref","unstructured":"Tseitin, G.: On the complexity of proofs in propositional logics, Seminars in Mathematics\n8 (1970). Reprinted in [33].","DOI":"10.1007\/978-1-4899-5327-8_25"},{"key":"395297_CR37","unstructured":"van Benthem, J.: Correspondence theory, in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, Volume II: Extensions of Classical Logic, Synthese Library 165, D. Reidel, Dordrecht, 1984, Chapter II.4, pp. 167\u2013247."},{"key":"395297_CR38","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1109\/LICS.1989.39179","volume-title":"Proceedings, Fourth Annual Symposium on Logic in Computer Science","author":"M. Y. Vardi","year":"1989","unstructured":"Vardi, M. Y.: On the complexity of epistemic reasoning, in Proceedings, Fourth Annual Symposium on Logic in Computer Science, Asilomar Conference Center, Pacific Grove, CA, 5\u20138 June 1989. IEEE Computer Society Press, 1989, pp. 243\u2013252."},{"key":"395297_CR39","doi-asserted-by":"crossref","unstructured":"Weidenbach, C., Gaede, B. and Rock, G.: SPASS & FLOTTER version 0.42, in M. A. McRobbie and J. K. Slaney (eds.), Proceedings of the 13th Conference on Automated Deduction (CADE-13), New Brunswick, NJ, July\/August 1996, Lecture Notes in Artificial Intelligence 1104, Springer, 1996, pp. 141\u2013145.","DOI":"10.1007\/3-540-61511-3_75"},{"key":"395297_CR40","doi-asserted-by":"crossref","unstructured":"Zhang, H.: SATO: An efficient propositional prover, in W. McCune (ed.), Proceedings of the 14th International Conference on Automated Deduction, Berlin, July 13\u201317, 1997, Lecture Notes in Artificial Intelligence 1249, Springer, 1997, pp. 272\u2013275.","DOI":"10.1007\/3-540-63104-6_28"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015071400913.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015071400913\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015071400913.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:35:34Z","timestamp":1749123334000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015071400913"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":40,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["395297"],"URL":"https:\/\/doi.org\/10.1023\/a:1015071400913","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}