{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:51:10Z","timestamp":1756000270719},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412854"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/3-540-44404-1_11","type":"book-chapter","created":{"date-parts":[[2007,11,13]],"date-time":"2007-11-13T19:20:51Z","timestamp":1194981651000},"page":"161-178","source":"Crossref","is-referenced-by-count":15,"title":["Equational Binary Decision Diagrams"],"prefix":"10.1007","author":[{"given":"Jan","family":"Groote","sequence":"first","affiliation":[]},{"given":"Jaco","family":"Pol","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","unstructured":"W. Ackermann. Solvable Cases of the Decision Problem. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1954. 162, 163, 175"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"H. R. Andersen and H. Hulgaard. Boolean expression diagrams. In Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 88\u201398, Warsaw, Poland, 1997. IEEE Computer Society. 164, 176","DOI":"10.1109\/LICS.1997.614938"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"F. Baader and T. Nipkow. Term Rewriting and All That. Cambridge University Press, 1998. 166","DOI":"10.1017\/CBO9781139172752"},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1002\/(SICI)1097-024X(200003)30:3<259::AID-SPE298>3.0.CO;2-Y","volume":"30","author":"M.G.J. Brand van den","year":"2000","unstructured":"M.G.J. van den Brand, H.A. de Jong, P. Klint, and P.A. Olivier. Efficient Annotated Terms. Software-Practice &amt; Experience, 30:259\u2013291, 2000. See also http:\/\/www.cwi.nl\/projects\/MetaEnv\/aterm\/ . 163, 175","journal-title":"Software-Practice &amt; Experience"},{"issue":"8","key":"11_CR5","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986. 161, 163","journal-title":"IEEE Transactions on Computers"},{"issue":"3","key":"11_CR6","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"R.E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, 1992. 161, 165","journal-title":"ACM Computing Surveys"},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","volume-title":"Exploiting positive equality in a logic of equality with uninterpreted functions","author":"R.E. Bryant","year":"1999","unstructured":"R.E. Bryant, S. German, and M.N. Velev. Exploiting positive equality in a logic of equality with uninterpreted functions. In N. Halbwachs and D Peled, editors, Proc. of Computer Aided Verification, CAV\u201999, LNCS 1633. Springer-Verlag, 1999. 161, 162, 163, 163, 164, 174"},{"key":"11_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Automatic verification of pipelined microprocessors control","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R. and D.L. Dill. Automatic verification of pipelined microprocessors control. In D. L. Dill, editor, Proceedings of Computer Aided Verification, CAV\u201994, LNCS 818, pages 68\u201380. Springer-Verlag, June 1994. 162, 163, 164"},{"issue":"1-2","key":"11_CR9","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3(1-2):69\u2013115, 1987. 166","journal-title":"Journal of Symbolic Computation"},{"key":"11_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"BDD based procedures for a theory of equality with uninterpreted functions","author":"A. Goel","year":"1998","unstructured":"A. Goel, K. Sajid, H. Zhou, and A. Aziz. BDD based procedures for a theory of equality with uninterpreted functions. In Proceedings of Computer Aided Verification, CAV\u201998, LNCS 1427, pages 244\u2013255. Springer-Verlag, 1998. 161, 164, 164, 164, 174"},{"key":"11_CR11","unstructured":"J.W. Klop. Term rewriting systems. In D. Gabbay S. Abramski and T. Maibaum, editors, Handbook of Logic in Computer Science, volume 1. Oxford University Press, 1991. 166"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"C. Meinel and T. Theobald. Algorithms and Data Structures in VLSI Design: OBDD-Foundations and Applications. Springer-Verlag, 1998. 161, 163, 165, 170","DOI":"10.1007\/978-3-642-58940-9"},{"key":"11_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_9","volume-title":"Computer Science Logic (CSL\u201999)","author":"J. M\u00f8ller","year":"1999","unstructured":"J. M\u00f8ller, J. Lichtenberg, H. R. Andersen, and H. Hulgaard. Difference decision diagrams. In J. Flum and M. Rodriguez-Artalejo, editors, Computer Science Logic (CSL\u201999), LNCS 1683. Springer-Verlag, 1999. 161, 164, 164, 164, 177"},{"issue":"2","key":"11_CR14","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/322186.322198","volume":"27","author":"G. Nelson","year":"1980","unstructured":"G. Nelson and D.C. Oppen. Fast decision procedures based on congruence closure. Journal of the Association for Computing Machinery, 27(2):356\u2013364, 1980. 163","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-61474-5_91","volume-title":"PVS: Combining specification, proof checking, and model checking","author":"S. Owre","year":"1996","unstructured":"S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Proceedings of Computer Aided Verification CAV\u201996, LNCS 1102, pages 411\u2013414. Springer-Verlag, 1996. 163"},{"key":"11_CR16","series-title":"Lect Notes Comput Sci","volume-title":"Deciding equality formulas by small domains instantiations","author":"A. Pnueli","year":"1999","unstructured":"A. Pnueli, Y. Rodeh, O. Shtrichman, and M. Siegel. Deciding equality formulas by small domains instantiations. In N. Halbwachs and D Peled, editors, Proceedings of Computer Aided Verification, CAV\u201999, LNCS 1633. Springer-Verlag, 1999. 161, 162, 163, 163, 163, 163, 174, 175, 175, 176, 176, 176"},{"key":"11_CR17","series-title":"Lect Notes Comput Sci","volume-title":"Binary decision diagrams by shared rewriting","author":"J.C. Pol van de","year":"2000","unstructured":"J.C. van de Pol and H. Zantema. Binary decision diagrams by shared rewriting. In M. Nielsen and B. Rovan, editors, Proceedings of Mathematical Foundations of Computer Science, MFCS\u201900, LNCS 1893. Springer-Verlag, 2000. 164"},{"issue":"7","key":"11_CR18","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1145\/359545.359570","volume":"21","author":"R.E. Shostak","year":"1978","unstructured":"R.E. Shostak. An algorithm for reasoning about equality. Communications of the ACM, 21(7):583\u2013585, 1978. 163, 165","journal-title":"Communications of the ACM"},{"key":"11_CR19","unstructured":"O. Shtrichman. Benchmarks for satisfiability checking of equality formulas. See http:\/\/www.wisdom.weizmann.ac.il\/\u00f5fers\/sat\/bench.htm , 1999. 163, 174, 175, 175, 175, 176, 176, 176"}],"container-title":["Lecture Notes in Artificial Intelligence","Logic for Programming and Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44404-1_11.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:23:54Z","timestamp":1619573034000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44404-1_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540412854"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-44404-1_11","relation":{},"subject":[]}}