{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T13:29:34Z","timestamp":1725542974411},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540372066"},{"type":"electronic","value":"9783540372073"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11814948_15","type":"book-chapter","created":{"date-parts":[[2006,7,18]],"date-time":"2006-07-18T06:12:38Z","timestamp":1153203158000},"page":"130-135","source":"Crossref","is-referenced-by-count":3,"title":["Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)\/ $\\mathcal{ALC}$"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Sebastiani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Vescovi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"S. Brand","year":"2003","unstructured":"Brand, S., Gennari, R., de Rijke, M.: Constraint Programming for Modelling and Solving Modal Satisfability. In: Rossi, F. (ed.) CP 2003. LNCS, vol.\u00a02833, Springer, Heidelberg (2003)"},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"Fitting, M.: Proof Methods for Modal and Intuitionistic Logics. D. Reidel Publishg (1983)","DOI":"10.1007\/978-94-017-2794-5"},{"key":"15_CR3","series-title":"Lecture Notes in Computer Science","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, vol.\u00a01104, Springer, Heidelberg (1996)"},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures - the case study of modal K(m). Information and Computation\u00a0162(1\/2) (2000)","DOI":"10.1006\/inco.1999.2850"},{"issue":"3","key":"15_CR5","first-page":"361","volume":"75","author":"J.Y. Halpern","year":"1995","unstructured":"Halpern, J.Y.: The effect of bounding the number of primitive propositions and the depth of nesting on the complexity of modal logic. AI\u00a075(3), 361\u2013372 (1995)","journal-title":"AI"},{"issue":"3","key":"15_CR6","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 the completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence\u00a054(3), 319\u2013379 (1992)","journal-title":"Artificial Intelligence"},{"issue":"3","key":"15_CR7","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1093\/logcom\/9.3.267","volume":"9","author":"I. Horrocks","year":"1999","unstructured":"Horrocks, I., Patel-Schneider, P.F.: Optimizing Description Logic Subsumption. Journal of Logic and Computation\u00a09(3), 267\u2013293 (1999)","journal-title":"Journal of Logic and Computation"},{"key":"15_CR8","unstructured":"Hustadt, U., Schmidt, R.A., Weidenbach, C.: MSPASS: Subsumption Testing with SPASS. In: Proc. DL 1999, pp. 136\u2013137 (1999)"},{"issue":"3","key":"15_CR9","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":"15_CR10","doi-asserted-by":"crossref","unstructured":"Massacci, F.: Single Step Tableaux for modal logics: methodology, computations, algorithms. Journal of Automated Reasoning\u00a0Vol. 24(3) (2000)","DOI":"10.1023\/A:1006155811656"},{"key":"15_CR11","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"G. Pan","year":"2002","unstructured":"Pan, G., Sattler, U., Vardi, M.Y.: BDD-Based Decision Procedures for K. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"},{"key":"15_CR12","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction \u2013 CADE-19","author":"G. Pan","year":"2003","unstructured":"Pan, G., Vardi, M.Y.: Optimizing a BDD-based modal solver. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, Springer, Heidelberg (2003)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Sebastiani, R., Vescovi, M.: Encoding the satisfiability of modal and description logics into SAT: the case study of K(m)\/ ${\\mathcal ALC}$ . Extended version. Technical Report DIT-06-033, DIT, University of Trento (May 2006), http:\/\/www.dit.unitn.it\/~rseba\/sat06\/extended.ps","DOI":"10.1007\/11814948_15"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2006"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11814948_15.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T03:27:53Z","timestamp":1619494073000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11814948_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540372066","9783540372073"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/11814948_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}