{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:16:03Z","timestamp":1742958963813,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540668220"},{"type":"electronic","value":"9783540466956"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-46695-9_30","type":"book-chapter","created":{"date-parts":[[2007,8,12]],"date-time":"2007-08-12T08:37:07Z","timestamp":1186907827000},"page":"353-364","source":"Crossref","is-referenced-by-count":1,"title":["Heuristics and Experiments on BDD Representation of Boolean Functions for Expert Systems in Software Verification Domains"],"prefix":"10.1007","author":[{"given":"Masahito","family":"Kurihara","sequence":"first","affiliation":[]},{"given":"Hisashi","family":"Kondo","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"30_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., Vol. C-27, No. 6, pp.509\u2013516 (1978)","journal-title":"IEEE Trans. Comput."},{"issue":"5","key":"30_CR2","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., Vol. C-35, No. 5, pp.677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"30_CR3","unstructured":"Bundy, A.: Rewrite rules, The Computer Modelling of Mathematical Reasoning, Academic Press, pp.115\u2013149 (1983)"},{"key":"30_CR4","unstructured":"Coudert, O. and Madre, J. C: Towards an interactive fault tree analyser, Proc. IASTED Int. Conf. on Reliability, Quality Control and Risk Assessment (1992)"},{"key":"30_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/3-540-15976-2_12","volume-title":"Proc. of 1st Conf. on Rewriting Techniques and Applications","author":"D. Detlefs","year":"1985","unstructured":"Detlefs, D. and Forgaad, R.: A procedure for automatically proving the termination of a set of rewrite rules, Proc. of 1st Conf. on Rewriting Techniques and Applications, Springer, LNCS 202, pp.255\u2013270 (1985)"},{"issue":"5","key":"30_CR6","first-page":"822","volume":"13","author":"H. Kondo","year":"1998","unstructured":"Kondo, H. and Kurihara, M.: Termination verification system for term rewriting systems using binary decision diagram, Intern. Journal of Japanese Society for Artificial Intelligence, Vol.13, No.5, pp.822\u2013834 (1998) (in Japanese)","journal-title":"Intern. Journal of Japanese Society for Artificial Intelligence"},{"issue":"4","key":"30_CR7","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, Vol.2, No.4, pp.547\u2013565 (1992)","journal-title":"Intern. Journal of Software Engineering and Knowledge Engineering"},{"key":"30_CR8","unstructured":"Kurihara, M. and Kondo, H.: Binary decision diagrams for mechanical verification of precedence-based termination of rewrite rules, Poster Proc. of 5th Pacific Rim Int. Conf. on Artificial Intelligence, pp.7\u201312 (1998)"},{"key":"30_CR9","unstructured":"Madre, J. C. and Coudert, O.: A logically complete reasoning maintenance system based on a logical constraint solver, Proc. IJCAI, pp.294\u2013299 (1991)"},{"key":"30_CR10","unstructured":"Malik, S., et al.: Logic verification using binary decision diagrams in a logic synthesis environment, Proc. IEEE Int. Conf. on Computer-Aided Design, pp.6\u20139 (1988)"},{"key":"30_CR11","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, Vol.12, pp.33\u201345 (1994)","journal-title":"Journal of Automated Reasoning"},{"key":"30_CR12","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":"30_CR13","volume-title":"Termination of rewriting","author":"J. Steinbach","year":"1994","unstructured":"Steinbach, J.: Termination of rewriting, Ph.D thesis, Univ. Kaiserslautern, Germany (1994)"},{"key":"30_CR14","series-title":"SEKI report","volume-title":"Check your ordering \u2014 termination proofs and open problems","author":"J. Steinbach","year":"1990","unstructured":"Steinbach, J. and K\u00fchler, U.: Check your ordering \u2014 termination proofs and open problems, SEKI report SR-90-25(SFB), Univ. Kaiserslautern, Germany (1990)"}],"container-title":["Lecture Notes in Computer Science","Advanced Topics in Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46695-9_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,29]],"date-time":"2024-11-29T01:02:36Z","timestamp":1732842156000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-46695-9_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540668220","9783540466956"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-46695-9_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}