{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T01:22:59Z","timestamp":1755220979991,"version":"3.43.0"},"reference-count":10,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2002,10,1]],"date-time":"2002-10-01T00:00:00Z","timestamp":1033430400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,10,1]],"date-time":"2002-10-01T00:00:00Z","timestamp":1033430400000},"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":["Studia Logica"],"published-print":{"date-parts":[[2002,10]]},"DOI":"10.1023\/a:1020530109551","type":"journal-article","created":{"date-parts":[[2003,3,18]],"date-time":"2003-03-18T15:12:43Z","timestamp":1048000363000},"page":"85-112","source":"Crossref","is-referenced-by-count":4,"title":["Satisfiability Testing for Boolean Formulas Using \u0394-trees"],"prefix":"10.1007","volume":"72","author":[{"given":"G.","family":"Guti\u00e9rrez","sequence":"first","affiliation":[]},{"given":"I. P.","family":"de Guzm\u00e1n","sequence":"additional","affiliation":[]},{"given":"J.","family":"Mart\u00ednez","sequence":"additional","affiliation":[]},{"given":"M.","family":"Ojeda-Aciego","sequence":"additional","affiliation":[]},{"given":"A.","family":"Valverde","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1\/2","key":"5106687_CR1","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1016\/S0304-3975(00)00044-X","volume":"266","author":"G. Aguilera","year":"2001","unstructured":"Aguilera, G., I. P. De Guzm\u00c1n, M. Ojeda-Aciego, and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science 266(1\/2):81-112, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"8","key":"5106687_CR2","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"Bryant, R. E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, C-35(8):677-691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"5106687_CR3","unstructured":"Claesen, L. J., editor. Formal VLSI correctness verification\u2014VLSI design methods, volume 2. Elsevier, 1990."},{"key":"5106687_CR4","unstructured":"Gallier, J. H.. Logic for Computer Science: Foundations for Automatic Theorem Proving. Wiley & Sons, 1987."},{"key":"5106687_CR5","doi-asserted-by":"crossref","unstructured":"Guti\u00c9rrez, G., I. P. De Guzm\u00c1n, J. Mart\u00cdnez, M. Ojeda-Aciego, and A. Valverde. Reduction theorems for Boolean formulas using \u0394-trees. In Proc. of JELIA 2000, pages 179-192. Lect. Notes in Artif. Intelligence 1919, 2000.","DOI":"10.1007\/3-540-40006-0_13"},{"key":"5106687_CR6","doi-asserted-by":"crossref","unstructured":"Massacci, F. Simplification: a general constraint propagation technique for propositional and modal tableaux. In Proceedings of Tableaux'98. Lect. Notes in Artificial Intelligence 1397, pages 217-231, 1998.","DOI":"10.1007\/3-540-69778-0_24"},{"issue":"3","key":"5106687_CR7","doi-asserted-by":"crossref","first-page":"504","DOI":"10.1145\/174130.174135","volume":"40","author":"N. V. Murray","year":"1993","unstructured":"Murray, N. V., and E. Rosenthal. Dissolution: Making paths vanish. Journal of the ACM, 40(3):504-535, 1993.","journal-title":"Journal of the ACM"},{"key":"5106687_CR8","doi-asserted-by":"crossref","unstructured":"Paulson, L. C. Isabelle: a generic theorem prover. Lect. Notes in Comp. Sci. 828, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"5106687_CR9","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1016\/0020-0255(94)90032-9","volume":"78","author":"P. W. Purdom Jr.","year":"1994","unstructured":"Purdom, Jr., P. W. Average time for the full pure literal rule. Information Sciences, 78:269-291, 1994.","journal-title":"Information Sciences"},{"key":"5106687_CR10","unstructured":"Yang, B., Y. A. Chen, R. E. Bryant, and D. R. O'Hallaron. Space-and time-efficient BDD construction via working set control. In Proceedings of Asian-Pacific Design Automation Conference ASPDAC '98, pages 423-432, 1998."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020530109551.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020530109551\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020530109551.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:29:55Z","timestamp":1754630995000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020530109551"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,10]]},"references-count":10,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2002,10]]}},"alternative-id":["5106687"],"URL":"https:\/\/doi.org\/10.1023\/a:1020530109551","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2002,10]]}}}