{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330215},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581567"},{"type":"electronic","value":"9783540484677"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58156-1_36","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:22:52Z","timestamp":1330269772000},"page":"499-513","source":"Crossref","is-referenced-by-count":4,"title":["Proving with BDDs and control of information"],"prefix":"10.1007","author":[{"given":"Jean","family":"Goubault","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"issue":"2","key":"36_CR1","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/322248.322249","volume":"28","author":"P. Andrews","year":"1981","unstructured":"P. Andrews. Theorem proving via general matings. JACM, 28(2):193\u2013214, 1981.","journal-title":"JACM"},{"key":"36_CR2","doi-asserted-by":"crossref","unstructured":"W. Bibel. Automated Theorem Proving. Vieweg, 2nd, revised edition, 1987.","DOI":"10.1007\/978-3-322-90102-6"},{"key":"36_CR3","unstructured":"J.-P. Billon. Perfect normal forms for discrete functions. Technical Report 87019, Bull, 1987."},{"issue":"8","key":"36_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean functions manipulation. IEEE Trans. Computers, C35(8):677\u2013692, 1986.","journal-title":"IEEE Trans. Computers"},{"key":"36_CR5","unstructured":"J. Goubault. Implementing functional languages with fast equality, sets and maps: an exercise in hash consing. Technical report, Bull, 1992."},{"key":"36_CR6","volume-title":"PhD thesis","author":"J. Goubault","year":"1993","unstructured":"J. Goubault. D\u00e9monstration automatique en logique classique: complexit\u00e9 et m\u00e9thodes. PhD thesis, \u00e9cole olytechnique, Palaiseau, France, 1993."},{"key":"36_CR7","unstructured":"J. Goubault. The HimML reference manual. Technical report, Bull, 1993."},{"key":"36_CR8","unstructured":"J. Goubault. Syntax independent connections. In D. et al.. Basin, editor, Workshop on Theorem Proving with Analytic Tableaux and Related Methods, number MPI-I-93-213. Max Planck Institut f\u00fcr Informatik, 1993."},{"key":"36_CR9","unstructured":"J. Goubault. A BDD-based skolemization procedure. In M. D'Agostino, editor, Workshop on Theorem Proving with Analytic Tableaux and Related Methods, 1994."},{"key":"36_CR10","doi-asserted-by":"crossref","unstructured":"J. Goubault. The complexity of resource-bounded first-order classical logic. In 11th STACS, 1994.","DOI":"10.1007\/3-540-57785-8_131"},{"issue":"4","key":"36_CR11","doi-asserted-by":"crossref","first-page":"572","DOI":"10.1145\/321906.321919","volume":"22","author":"R. Kowalski","year":"1975","unstructured":"R. Kowalski. A proof procedure using connection graphs. JACM, 22(4):572\u2013595, 1975.","journal-title":"JACM"},{"key":"36_CR12","doi-asserted-by":"crossref","first-page":"227","DOI":"10.1016\/0004-3702(71)90012-9","volume":"2","author":"R. Kowalski","year":"1971","unstructured":"R. Kowalski and D. Kuehner. Linear resolution with selection function. Artificial Intelligence, 2:227\u2013260, 1971.","journal-title":"Artificial Intelligence"},{"key":"36_CR13","doi-asserted-by":"crossref","unstructured":"R. Manthey and F. Bry. SATCHMO: a theorem prover implemented in Prolog. In 9th CADE, pages 415\u2013434, 1988.","DOI":"10.1007\/BFb0012847"},{"issue":"2","key":"36_CR14","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"A. Martelli and U. Montanari. An efficient unification algorithm. ACM TOPLAS, 4(2):258\u2013282, 1982.","journal-title":"ACM TOPLAS"},{"key":"36_CR15","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F. J. Pelletier. Seventy-five problems for testing automatic theorem provers. JAR, 2:191\u2013216, 1986. Errata in JAR, 4:235\u2013236, 1988.","journal-title":"JAR"},{"key":"36_CR16","first-page":"4","volume":"6","author":"F. J. Pelletier","year":"1986","unstructured":"F. J. Pelletier and P. Rudnicki. Non-obviousness. AAR Newsl., 6:4\u20135, 1986.","journal-title":"AAR Newsl."},{"key":"36_CR17","volume-title":"PhD thesis","author":"J. Posegga","year":"1993","unstructured":"J. Posegga. Deduction with Shannon Graphs or: How to Lift BDDs to First-order Logic. PhD thesis, Institut f\u00fcr Logik, Komplexit\u00e4t und Deduktionssystem, Universit\u00e4t Karlsruhe, Karlsruhe, FRG, 1993."},{"key":"36_CR18","unstructured":"C. E. Shannon and W. Weaver. The Mathematical Theory of Communication. Illinois University Press, 1949. Reprinted by Illini Books, 1963."},{"issue":"4","key":"36_CR19","doi-asserted-by":"crossref","first-page":"536","DOI":"10.1145\/321296.321302","volume":"12","author":"L. Wos","year":"1965","unstructured":"L. Wos, G. A. Robinson, and D. F. Carson. Efficiency and completeness of the set of support strategy in theorem proving. JACM, 12(4):536\u2013541, 1965.","journal-title":"JACM"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2014 CADE-12"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58156-1_36.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:38Z","timestamp":1605647858000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58156-1_36"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581567","9783540484677"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-58156-1_36","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}