{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T06:05:48Z","timestamp":1747548348484,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540673507"},{"type":"electronic","value":"9783540462385"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46238-4_9","type":"book-chapter","created":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T02:05:23Z","timestamp":1185933923000},"page":"95-106","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["The SAT-Based Approach for Classical Modal Logics"],"prefix":"10.1007","author":[{"given":"Enrico","family":"Giunchiglia","sequence":"first","affiliation":[]},{"given":"Fausto","family":"Giunchiglia","sequence":"additional","affiliation":[]},{"given":"Armando","family":"Tacchella","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,12,15]]},"reference":[{"key":"9_CR1","unstructured":"E. Giunchiglia, F. Giunchiglia, R. Sebastiani, and A. Tacchella. More evaluation of decision procedures for modal logics. In Proc. KR\u201998, Trento, Italy, June 1998."},{"key":"9_CR2","unstructured":"F. Giunchiglia and R. Sebastiani. Building decision procedures for modal logics from propositional decision procedures-the case study of modal K. In Proc. CADE-96, LNAI. Springer Verlag."},{"key":"9_CR3","unstructured":"F. Giunchiglia and R. Sebastiani. A SAT-based decision procedure for ALC. In Proc. of KR\u201996, Cambridge, MA, USA, November 1996."},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"H. Zhang. SATO: An efficient propositional prover. In William McCune, editor, Proc. CADE-14, volume 1249 of LNAI, pages 272\u2013275, 1997. Springer.","DOI":"10.1007\/3-540-63104-6_28"},{"key":"9_CR5","unstructured":"E. Giunchiglia, F. Giunchiglia, and A. Tacchella. *SAT, KSATC, DLP and TA: a comparative analysis. In Collected Papers from the International Description Logics Workshop (DL\u201999). CEUR, July 1999."},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"B. F. Chellas. Modal Logic\u2013an Introduction. Cambridge University Press, 1980.","DOI":"10.1017\/CBO9780511621192"},{"key":"9_CR7","first-page":"102","volume-title":"Contemporary Philosophy: A Survey. I","author":"R. Montague","year":"1968","unstructured":"Richard Montague. Pragmatics. In R. Klibansky, editor, Contemporary Philosophy: A Survey. I, pages 102\u2013122. La Nuova Italia Editrice, Florence, 1968."},{"key":"9_CR8","volume-title":"An Essay in Classical Modal Logic","author":"K. Segerberg","year":"1971","unstructured":"Krister Segerberg. An Essay in Classical Modal Logic. Philosophical Studies, Uppsala, 1 edition, 1971.","edition":"1 edition"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"R. Fagin, J.Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about knowledge. MIT Press, 1995.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"9_CR10","series-title":"Technical Report","volume-title":"From Tableau-based to SAT-based procedures-preliminary report","author":"R. Sebastiani","year":"1997","unstructured":"R. Sebastiani and F. Giunchiglia. From Tableau-based to SAT-based procedures-preliminary report. Technical Report 9711-14, IRST, Trento, Italy, 1997."},{"key":"9_CR11","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1145\/321033.321034","volume":"7","author":"M. Davis","year":"1960","unstructured":"M. Davis and H. Putnam. A computing procedure for quantification theory. Journal of the ACM, 7:201\u2013215, 1960.","journal-title":"Journal of the ACM"},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"Moshe Y. Vardi. On the complexity of epistemic reasoning. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 243\u2013252. IEEE Computer Society Press.","DOI":"10.1109\/LICS.1989.39179"},{"key":"9_CR13","unstructured":"Armando Tacchella. *SAT system description. In Collected Papers from the International Description Logics Workshop (DL\u201999). CEUR, July 1999."},{"key":"9_CR14","unstructured":"E. Franconi, G. De Giacomo, R. M. MacGregor, W. Nutt, C. A. Welty, and F. Sebastiani, editors. Collected Papers from the International Description Logics Workshop (DL\u201998). CEUR, May 1998."},{"key":"9_CR15","unstructured":"H. de Swart, editor. Automated Reasoning with Analytic Tableaux and Related Methods: International Conference Tableaux\u201998, number 1397 in LNAI. Springer."},{"key":"9_CR16","doi-asserted-by":"crossref","unstructured":"O. Gasquet and A. Herzig. From classical to normal modal logics. In Heinrich Wansing, editor, Proof Theory of Modal Logics, volume 2 of Applied Logic Series, pages 293\u2013311. Kluwer Academic Publishers, 1996.","DOI":"10.1007\/978-94-017-2798-3_15"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"M. Fitting. Proof Methods for Modal and Intuitionistic Logics. D. Reidel Publishing, 1983.","DOI":"10.1007\/978-94-017-2794-5"},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"G. Governatori and A. Luppi. Labelled tableaux for non-normal modal logics. In Proc. AI*IA\u2019 99, Bologna, Italy, September 14\u201317, 1999.","DOI":"10.1007\/3-540-46238-4_11"},{"key":"9_CR19","unstructured":"P. F. Patel-Schneider. DLP system description. In E. Franconi, G. De Giacomo, R. M. MacGregor, W. Nutt, C. A. Welty, and F. Sebastiani, editors, Collected Papers from the International Description Logics Workshop (DL\u201998), pages 87\u201389. CEUR, May 1998."},{"key":"9_CR20","unstructured":"U. Hustadt and R.A. Schmidt. On evaluating decision procedures for modal logic. In Proc. IJCAI-15, 1997."},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"C. Weidenbach, B. Gaede, and G. Rock. SPASS & FLOTTER version 0.42. In M.A. McRobbie and J.K. Slaney, editors, Proc. CADE-13, volume 1104 of LNAI, pages 141\u2013145, New Brunswick, New Jersey, USA, July\/August 1996. Springer.","DOI":"10.1007\/3-540-61511-3_75"}],"container-title":["Lecture Notes in Computer Science","AI*IA 99: Advances in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46238-4_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T01:35:27Z","timestamp":1737336927000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46238-4_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540673507","9783540462385"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/3-540-46238-4_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"15 December 2000","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}