{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:48:48Z","timestamp":1762458528215},"reference-count":58,"publisher":"Informa UK Limited","issue":"1-2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Applied Non-Classical Logics"],"published-print":{"date-parts":[[2006,1]]},"DOI":"10.3166\/jancl.16.169-207","type":"journal-article","created":{"date-parts":[[2007,4,11]],"date-time":"2007-04-11T13:14:19Z","timestamp":1176297259000},"page":"169-207","source":"Crossref","is-referenced-by-count":18,"title":["BDD-based decision procedures for the modal logic K \u2605"],"prefix":"10.1080","volume":"16","author":[{"given":"Guoqiang","family":"Pan","sequence":"first","affiliation":[{"name":"a   Department of Computer Science , Rice University ,  Houston ,  Texas ,  77005 ,  USA"}]},{"given":"Ulrike","family":"Sattler","sequence":"additional","affiliation":[{"name":"b   School of Computer Science , University of Manchester , Oxford Road,  Manchester ,  M13 9PL ,  UK"}]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[{"name":"a   Department of Computer Science , Rice University ,  Houston ,  Texas ,  77005 ,  USA"}]}],"member":"301","published-online":{"date-parts":[[2012,4,13]]},"reference":[{"key":"CIT0001","volume-title":"An Introduction to Binary Decision Diagrams","author":"ANDERSEN H.","year":"1998"},{"key":"CIT0002","first-page":"199","volume-title":"Proc. of the 14th Eur. Conf. on Artif. Int","author":"ARECES C."},{"key":"CIT0003","first-page":"92","volume-title":"Proc. 1st Int. Joint Conf. Automated Reasoning, vol. 2083 of LNCS","author":"BAADER F."},{"key":"CIT0004","first-page":"182","volume-title":"Proc. 6th Conf. on CAV, vol. 818 of LNCS","author":"BEER I.","year":"1994"},{"key":"CIT0005","volume-title":"Tools and Algorithms for the Analysis and Construction of Systems, vol. 1579 of Lecture Notes in Computer Science","author":"BIERE A.","year":"1999"},{"key":"CIT0006","first-page":"238","volume-title":"Proc. 7th Int. Conf. on Theory and Applications of Satisfiability Testing (SAT 2004)","author":"BIERE A."},{"key":"CIT0007","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"CIT0008","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1109\/TC.1982.1675978","volume":"31","author":"BOCHMANN G. V.","year":"1982","journal-title":"IEEE Transactions on Computers"},{"key":"CIT0009","first-page":"208","volume-title":"Theoretical Aspects of Reasoning about Knowledge: Proc. Fifth Conference","author":"BRAFMAN R."},{"key":"CIT0010","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"issue":"1","key":"CIT0011","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"BUNING H.","year":"1995","journal-title":"Inf. and Comp."},{"key":"CIT0012","first-page":"325","volume-title":"Proc. 2nd Conference on Theoretical Aspects of Reasoning about Knowledge","author":"BURROWS M."},{"key":"CIT0013","first-page":"49","volume-title":"VLSI 91, Proc. IFIP TC10\/WG 10.5 International Conference on Very Large Scale Integration","author":"BURCH J. R."},{"key":"CIT0014","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"CIT0015","volume-title":"An algorithm to evaluate quantified Boolean formulae and its experimental evaluation","author":"CADOLI M.","year":"1999"},{"key":"CIT0016","first-page":"280","volume-title":"Proc. 8th Int. Conf. on Very Large Data Bases","author":"CASTILHO J. M. V."},{"issue":"4","key":"CIT0017","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/s100090050046","volume":"2","author":"CIMATTI A.","year":"2000","journal-title":"Int. J. on Software Tools for Tech. Transfer"},{"key":"CIT0018","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"CIT0019","first-page":"143","volume-title":"Proc. of the Int. Conf. on Constraint Prog. (CP 2000)","author":"COARFA C."},{"key":"CIT0020","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"key":"CIT0021","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"CIT0022","first-page":"153","volume-title":"CONCUR 2000 - Concurrency Theory, 11th Int. Conf","author":"ETESSAMI K."},{"key":"CIT0023","first-page":"299","volume-title":"Proc. 6th Int. Conf. on Computer Aided Verification (CAV 1994)","author":"GEIST D."},{"key":"CIT0024","first-page":"648","volume-title":"AAAI: 16th National Conference on Artificial Intelligence","author":"GENT I."},{"key":"CIT0025","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1006\/inco.1999.2850","volume":"162","author":"GIUNCHIGLIA F.","year":"2000","journal-title":"Inf. and Comp."},{"key":"CIT0026","first-page":"364","volume-title":"Automated Reasoning, First Int. Joint Conf., IJCAR 2001","author":"GIUNCHIGLIA E."},{"key":"CIT0027","volume-title":"Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence (IJCAI-01)","volume":"1847","author":"HAARSLEV V."},{"key":"CIT0028","doi-asserted-by":"publisher","DOI":"10.1145\/79147.79161"},{"key":"CIT0029","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(92)90049-4"},{"key":"CIT0030","volume-title":"A benchmark method for the propositional modal logics K, KT, S4","author":"HEUERDING A.","year":"1996"},{"key":"CIT0031","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.3.239"},{"key":"CIT0032","first-page":"67","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Int. Conf., TABLEAUX 2000","author":"HUSTADT U."},{"key":"CIT0033","first-page":"359","volume-title":"International Conference on Computer-Aided Design (ICCAD 1998)","author":"KAMHI G."},{"key":"CIT0034","first-page":"290","volume-title":"Formal Methods in Computer-Aided Design, Second International Conference FMCAD'98, vol. 1522 of LNCS","author":"KAMHI G."},{"key":"CIT0035","doi-asserted-by":"publisher","DOI":"10.1137\/0206033"},{"key":"CIT0036","first-page":"160","author":"LETZ R.","year":"2002","journal-title":"TABLEAUX 2002"},{"key":"CIT0037","first-page":"374","volume-title":"Proc. 6th International Symposium on Mathematical Foundations of Computer Science","volume":"53","author":"LIPSKI W."},{"key":"CIT0038","first-page":"52","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Int. Conf., TABLEAUX 2000","author":"MASSACCI F."},{"key":"CIT0039","first-page":"463","volume-title":"Machine Intelligence 4","author":"MCCARTHY J.","year":"1969"},{"key":"CIT0040","first-page":"453","volume-title":"Proceedings of 10th Int. Conf. on Principles and Practice of Constraint Programming (CP 2004)","author":"PAN G."},{"key":"CIT0041","first-page":"19","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods, Int. Conf., TABLEAUX '99","author":"PATEL-SCHNEIDER P."},{"key":"CIT0042","first-page":"464","volume-title":"Automated Reasoning, First Int. Joint Conf., IJCAR 2001","author":"PATEL-SCHNEIDER P."},{"key":"CIT0043","first-page":"46","volume-title":"Proc. 18th IEEE Symp. on Foundation of Computer Science","author":"PNUELI A."},{"key":"CIT0044","first-page":"109","volume-title":"Proc. 17th IEEE Symp. on Foundations of Computer Science","author":"PRATT V. R."},{"key":"CIT0045","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(80)90061-6"},{"key":"CIT0046","volume-title":"Proc. of IEEE\/ACM Int. Workshop on Logic Synthesis","author":"RANJAN R."},{"key":"CIT0047","first-page":"629","volume-title":"Proc. 12th International Colloq. on Automata, Languages, and Programming","volume":"104","author":"REIF J. H."},{"key":"CIT0048","first-page":"323","volume":"10","author":"RINTANEN J.","year":"1999","journal-title":"J. of A. I. Res."},{"key":"CIT0049","first-page":"42","volume-title":"International Conference on Computer-Aided Design (ICCAD 1993)","author":"RUDELL R."},{"key":"CIT0050","first-page":"121","volume-title":"Principles and Practice of Constraint Programming - CP 2001, 7th Int. Conf","author":"SAN MIGUEL AGUIRRE A."},{"issue":"1","key":"CIT0051","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(95)00045-3","volume":"81","author":"SELMAN B.","year":"1996","journal-title":"Artificial Intelligence"},{"key":"CIT0052","volume-title":"CUDD: CU Decision Diagram package","author":"SOMENZI F.","year":"1998"},{"key":"CIT0053","first-page":"247","volume-title":"Computer Aided Verification, 12th Int. Conf., CAV 2000","author":"SOMENZI F."},{"key":"CIT0054","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"STOCKMEYER L.","year":"1977","journal-title":"Theo. Comp. Sci."},{"key":"CIT0055","volume-title":"Proceedings of the Intl. Workshop Description Logics 1999","author":"TACCHELLA A."},{"key":"CIT0056","first-page":"389","volume-title":"Algorithms and Computation, 4th International Symposium, ISAAC '93","author":"TANI S."},{"key":"CIT0057","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1090\/dimacs\/031\/05","volume-title":"Descriptive Complexity and Finite Models","author":"VARDI M.","year":"1997"},{"issue":"2","key":"CIT0058","first-page":"182","volume":"2","author":"VORONKOV A.","year":"2001","journal-title":"Comp. Logic"}],"container-title":["Journal of Applied Non-Classical Logics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.3166\/jancl.16.169-207","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,23]],"date-time":"2017-06-23T14:27:28Z","timestamp":1498228048000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.3166\/jancl.16.169-207"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":58,"journal-issue":{"issue":"1-2","published-online":{"date-parts":[[2012,4,13]]},"published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.3166\/jancl.16.169-207"],"URL":"https:\/\/doi.org\/10.3166\/jancl.16.169-207","relation":{},"ISSN":["1166-3081","1958-5780"],"issn-type":[{"value":"1166-3081","type":"print"},{"value":"1958-5780","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,1]]}}}