{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T19:29:23Z","timestamp":1725564563390},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540220077"},{"type":"electronic","value":"9783540246770"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24677-0_85","type":"book-chapter","created":{"date-parts":[[2010,9,8]],"date-time":"2010-09-08T21:37:46Z","timestamp":1283981866000},"page":"827-837","source":"Crossref","is-referenced-by-count":11,"title":["Efficient BDD Encodings for Partial Order Constraints with Application to Expert Systems in Software Verification"],"prefix":"10.1007","author":[{"given":"Masahito","family":"Kurihara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hisashi","family":"Kondo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"6","key":"85_CR1","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S.B. Akers","year":"1978","unstructured":"Akers, S.B.: Binary decision diagrams. IEEE Trans. Comput.\u00a0C-27(6), 509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"key":"85_CR2","doi-asserted-by":"publisher","first-page":"993","DOI":"10.1109\/12.537122","volume":"45","author":"B. Bollig","year":"1996","unstructured":"Bollig, B., Wegener, I.: Improving the variable ordering of OBDDs is NP-complete. IEEE Trans. on Computers\u00a045, 993\u20131002 (1996)","journal-title":"IEEE Trans. on Computers"},{"issue":"5","key":"85_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithm for boolean function manipulation. IEEE Trans. Comput.\u00a0C-35(5), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"85_CR4","unstructured":"Coudert, O., Madre, J.C.: Towards an interactive fault tree analyser. In: Proc. IASTED Int. Conf. on Reliability, Quality Control and Risk Assessment (1992)"},{"key":"85_CR5","first-page":"243","volume-title":"Handbook of Theoretical Computer Science","author":"N. Dershowitz","year":"1990","unstructured":"Dershowitz, N., Jouannaud, J.-P.: Rewrite Systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 243\u2013320. North-Holland, Amsterdam (1990)"},{"key":"85_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"255","DOI":"10.1007\/3-540-15976-2_12","volume-title":"Rewriting Techniques and Applications","author":"D. Detlefs","year":"1985","unstructured":"Detlefs, D., Forgaad, R.: A procedure for automatically proving the termination of a set of rewrite rules. In: Jouannaud, J.-P. (ed.) RTA 1985. LNCS, vol.\u00a0202, pp. 255\u2013270. Springer, Heidelberg (1985)"},{"key":"85_CR7","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/43.184839","volume":"12","author":"M. Fujita","year":"1993","unstructured":"Fujita, M., Fujisawa, H., Matsunaga, Y.: Variable ordering algorithms for ordered binary decision diagrams and their evaluation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems\u00a012, 6\u201312 (1993)","journal-title":"IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"4","key":"85_CR8","doi-asserted-by":"publisher","first-page":"547","DOI":"10.1142\/S0218194092000257","volume":"2","author":"M. Kurihara","year":"1992","unstructured":"Kurihara, M., Kondo, H., et al.: Using ATMS to efficiently verify the termination of rewrite rule programs, Intern. Journal of Software Engineering and Knowledge Engineering\u00a02(4), 547\u2013565 (1992)","journal-title":"Journal of Software Engineering and Knowledge Engineering"},{"key":"85_CR9","unstructured":"Madre, J.C., Coudert, O.: A logically complete reasoning maintenance system based on a logical constraint solver. In: Proc. Intern. Joint Conf. on Artificial Intelligence, pp. 294\u2013299 (1991)"},{"key":"85_CR10","unstructured":"Malik, S., et al.: Logic verification using binary decision diagrams in a logic synthesis environment. In: Proc. IEEE Int. Conf. on Computer-Aided Design, pp. 6\u20139 (1988)"},{"key":"85_CR11","doi-asserted-by":"crossref","unstructured":"Minato, S., Ishiura, N., Yajima, S.: Shared binary decision diagram with attributed edges for efficient Boolean function manipulation. In: 27th DAC, pp. 52\u201357 (1990)","DOI":"10.1145\/123186.123225"},{"key":"85_CR12","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BF00881842","volume":"12","author":"J.S. Moore","year":"1994","unstructured":"Moore, J.S.: Introduction to the OBDD algorithm for the ATP community. Journal of Automated Reasoning\u00a012, 33\u201345 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"85_CR13","doi-asserted-by":"crossref","unstructured":"Plaisted, D.A.: Equational reasoning and term rewriting systems. In: Gabbay, D.M. (ed.) Handbook of Logic in Artificial Intelligence and Logic Programming, pp. 274\u2013364 (1993)","DOI":"10.1093\/oso\/9780198537458.003.0005"},{"key":"85_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/BFb0028562","volume-title":"STACS 98","author":"D. Sieling","year":"1998","unstructured":"Sieling, D.: On the existence of polynomial time approximation schemes for OBDD minimization. In: Meinel, C., Morvan, M. (eds.) STACS 1998. LNCS, vol.\u00a01373, pp. 205\u2013215. Springer, Heidelberg (1998)"},{"key":"85_CR15","unstructured":"Steinbach, J.: Termination of rewriting: Ph.D thesis, Univ. Kaiserslautern, Germany (1994)"},{"key":"85_CR16","unstructured":"Steinbach, J., K\u00fchler, U.: Check your ordering: termination proofs and open problems, SEKI report SR-90-25(SFB), Univ. Kaiserslautern, Germany (1990)"},{"key":"85_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"389","DOI":"10.1007\/3-540-57568-5_270","volume-title":"Algorithms and Computation","author":"S. Tani","year":"1993","unstructured":"Tani, S., Hamaguchi, K., Yajima, S.: The complexity of the optimal variable ordering problem of a shared binary decision diagram. In: Ng, K.W., Balasubramanian, N.V., Raghavan, P., Chin, F.Y.L. (eds.) ISAAC 1993. LNCS, vol.\u00a0762, pp. 389\u2013398. Springer, Heidelberg (1993)"},{"key":"85_CR18","doi-asserted-by":"crossref","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams: Theory and Application. Society for Industrial and Applied Mathematics (2000)","DOI":"10.1137\/1.9780898719789"}],"container-title":["Lecture Notes in Computer Science","Innovations in Applied Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24677-0_85.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,30]],"date-time":"2024-03-30T07:19:04Z","timestamp":1711783144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24677-0_85"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540220077","9783540246770"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24677-0_85","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}