{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:06:33Z","timestamp":1725663993191},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540584506"},{"type":"electronic","value":"9783540488033"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58450-1_47","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:10:35Z","timestamp":1330254635000},"page":"254-268","source":"Crossref","is-referenced-by-count":0,"title":["Binary decision diagrams as a HOL derived rule"],"prefix":"10.1007","author":[{"given":"John","family":"Harrison","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"17_CR1","first-page":"1259","volume":"3","author":"G. M. Adel'son-Vel'skii","year":"1986","unstructured":"G. M. Adel'son-Vel'skii and E. M. Landis. An algorithm for the organization of information. Soviet Mathematics Doklady, 3:1259\u20131263, 1986.","journal-title":"Soviet Mathematics Doklady"},{"key":"17_CR2","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. B. Akers","year":"1978","unstructured":"S. B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27:509\u2013516, 1978.","journal-title":"IEEE Transactions on Computers"},{"key":"17_CR3","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1007\/BF01459101","volume":"99","author":"P. Bernays","year":"1928","unstructured":"P. Bernays and M. Sch\u00f6nfinkel. Zum entscheidungsproblem der mathematischen logik. Mathematische Annalen, 99:401\u2013419, 1928.","journal-title":"Mathematische Annalen"},{"doi-asserted-by":"crossref","unstructured":"Karl S. Brace, Richard L. Rudell, and Randall E. Bryant. Efficient implementation of abdd package. Proceedings of 27th ACM\/IEEE Design Automation Conference, pages 40\u201345, 1990.","key":"17_CR4","DOI":"10.1145\/123186.123222"},{"key":"17_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Randall E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35:677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"crossref","unstructured":"S. A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd ACM Symposium on the Theory of Computing, pages 151\u2013158, 1971.","key":"17_CR6","DOI":"10.1145\/800157.805047"},{"unstructured":"M. Fujita, H. Fujisawa, and N. Kawato. Evaluations and improvements of a boolean comparison program based on binary decision diagrams. In Proceedings of the International Conference on Computer-Aided Design, pages 2\u20135. IEEE, 1988.","key":"17_CR7"},{"unstructured":"John Harrison and Laurent Th\u00e9ry. Reasoning about the reals: the marriage of hol and maple. In Logic programming and automated reasoning: proceedings of the 4th international conference, LPAR '93, volume 698 of Lecture Notes in Artificial Intelligence, pages 351\u2013353. Springer-Verlag, 1992.","key":"17_CR8"},{"doi-asserted-by":"crossref","unstructured":"John Harrison and Laurent Th\u00e9ry. Extending the hol theorem prover with a computer algebra system to reason about the reals. In Proceedings of the 1993 International Workshop on the HOL theorem proving system and its applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, 1994.","key":"17_CR9","DOI":"10.1007\/3-540-57826-9_134"},{"unstructured":"D. Hilbert and W. Ackermann. Principles of Mathematical Logic. Chelsea, 1950.","key":"17_CR10"},{"key":"17_CR11","doi-asserted-by":"crossref","first-page":"985","DOI":"10.1002\/j.1538-7305.1959.tb01585.x","volume":"38","author":"C. Y. Lee","year":"1959","unstructured":"C. Y. Lee. Representation of switching circuits by binary-decision programs. Bell System Technical Journal, 38:985\u2013999, 1959.","journal-title":"Bell System Technical Journal"},{"doi-asserted-by":"crossref","unstructured":"S. Malik, A. Wang, R. K. Brayton, and A. Sangiovanni-Vincentelli. Logic verification using binary decision diagrams in a logic synthesis environment. In Proceedings of the International Conference on Computer-Aided Design, pages 6\u20139. IEEE, 1988.","key":"17_CR12","DOI":"10.1109\/ICCAD.1988.122451"},{"unstructured":"A. Tarski. Undecidable Theories. Studies in Logic and the Foundations of Mathematics. North-Holland, 1953.","key":"17_CR13"},{"unstructured":"Diederik Verkest and Luc Claesen. Special benchmark session on tautology checking. In Formal VLSI Correctness Verification, pages 81\u201382. Elsevier Science Publishers, 1990.","key":"17_CR14"}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58450-1_47.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:21:29Z","timestamp":1605630089000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58450-1_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540584506","9783540488033"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/3-540-58450-1_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}