{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T23:38:42Z","timestamp":1725838722527},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319263496"},{"type":"electronic","value":"9783319263502"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-26350-2_19","type":"book-chapter","created":{"date-parts":[[2015,11,21]],"date-time":"2015-11-21T10:59:35Z","timestamp":1448103575000},"page":"218-228","source":"Crossref","is-referenced-by-count":0,"title":["Implementing Modal Tableaux Using Sentential Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Gor\u00e9","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jason Jingshi","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Pagram","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,11,22]]},"reference":[{"issue":"3","key":"19_CR1","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1006249507577","volume":"24","author":"P Balsiger","year":"2000","unstructured":"Balsiger, P., Heuerding, A., Schwendimann, S.: A benchmark method for the propositional modal logics K, KT, S4. J. Automat. Reason. 24(3), 297\u2013317 (2000)","journal-title":"J. Automat. Reason."},{"key":"19_CR2","volume-title":"Modal Logic","author":"P Blackburn","year":"2002","unstructured":"Blackburn, P., De Rijke, M., Venema, Y.: Modal Logic. Cambridge University Press, Cambridge (2002)"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Choi, A., Darwiche, A.: Dynamic minimization of sentential decision diagrams. In: AAAI (2013)","DOI":"10.1609\/aaai.v27i1.8690"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Cook, S.A.: The complexity of theorem-proving procedures. In: ACM (1971)","DOI":"10.1145\/800157.805047"},{"key":"19_CR5","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: IJCAI (2011)"},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"19_CR7","unstructured":"Een, N., S\u00f6rensson, N.: MiniSat: a SAT solver with conflict-clause minimization. In: SAT (2005)"},{"key":"19_CR8","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"2003","unstructured":"Fagin, R., Moses, Y., Halpern, J.Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (2003)"},{"key":"19_CR9","unstructured":"Girle, R.: Modal Logics and Philosophy (2000)"},{"key":"19_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-94-017-1754-0_6","volume-title":"Handbook of Tableau Methods","author":"R Gor\u00e9","year":"1999","unstructured":"Gor\u00e9, R.: Tableau methods for modal and temporal logics. In: D\u2019Agostino, M., Gabbay, D.M., H\u00e4hnle, R., Posegga, J. (eds.) Handbook of Tableau Methods, pp. 297\u2013396. Springer, Amsterdam (1999)"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-319-08587-6_25","volume-title":"Automated Reasoning","author":"R Gor\u00e9","year":"2014","unstructured":"Gor\u00e9, R., Olesen, K., Thomson, J.: Implementing tableau calculi using BDDs: BDDTab system description. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS, vol. 8562, pp. 337\u2013343. Springer, Heidelberg (2014)"},{"key":"19_CR12","unstructured":"Hoos, H., Stiitzle, T.: Satlib: an online resource for research on SAT (2000)"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/978-3-642-38574-2_31","volume-title":"Automated Deduction \u2013 CADE-24","author":"M Kaminski","year":"2013","unstructured":"Kaminski, M., Tebbi, T.: InKreSAT: modal reasoning via incremental reduction to SAT. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 436\u2013442. Springer, Heidelberg (2013)"},{"key":"19_CR14","volume-title":"Automated Theorem Proving: A Logical Basis","author":"DW Loveland","year":"2014","unstructured":"Loveland, D.W.: Automated Theorem Proving: A Logical Basis. Elsevier, Toronto (2014)"},{"key":"19_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/11814771_26","volume-title":"Automated Reasoning","author":"D Tsarkov","year":"2006","unstructured":"Tsarkov, D., Horrocks, I.: FaCT++ description logic reasoner: system description. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 292\u2013297. Springer, Heidelberg (2006)"},{"key":"19_CR16","unstructured":"UCLA: The SDD Package 1.1.1 (2014). http:\/\/hreasoning.cs.ucla.edu\/sdd\/"}],"container-title":["Lecture Notes in Computer Science","AI 2015: Advances in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-26350-2_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,8,15]],"date-time":"2023-08-15T22:54:43Z","timestamp":1692140083000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-26350-2_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319263496","9783319263502"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-26350-2_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}