{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:27:01Z","timestamp":1725488821720},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540411314"},{"type":"electronic","value":"9783540400066"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40006-0_13","type":"book-chapter","created":{"date-parts":[[2007,8,11]],"date-time":"2007-08-11T13:41:54Z","timestamp":1186839714000},"page":"179-192","source":"Crossref","is-referenced-by-count":1,"title":["Reduction Theorems for Boolean Formulas Using \u0394-Trees"],"prefix":"10.1007","author":[{"given":"Gloria","family":"Guti\u00e9rrez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Inma P.","family":"de Guzm\u00e1n","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Javier","family":"Mart\u00ednez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Manuel","family":"Ojeda-Aciego","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Agust\u00edn","family":"Valverde","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,9,19]]},"reference":[{"issue":"1","key":"13_CR1","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1080\/11663081.1995.10510841","volume":"5","author":"G. Aguilera","year":"1995","unstructured":"G. Aguilera, I. P. de Guzm\u00e1n, and M. Ojeda-Aciego. Increasing the efficiency of automated theorem proving. Journal of Applied Non-Classical Logics, 5(1):9\u201329, 1995.","journal-title":"Journal of Applied Non-Classical Logics"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"G. Aguilera, I. P. de Guzm\u00e1n, M. Ojeda-Aciego, and A. Valverde. Reductions for non-clausal theorem proving. Theoretical Computer Science, 2000. To appear. Available at http:\/\/www.ctima.uma.es\/aciego\/TR\/TAS-tcs.pdf .","DOI":"10.1016\/S0304-3975(00)00044-X"},{"key":"13_CR3","unstructured":"L.J. Claesen, editor. Formal VLSI correctness verification\u2014VLSI design methods, volume 2. Elsevier, 1990."},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1023\/A:1018923315631","volume":"27","author":"I. P. Guzm\u00e1n de","year":"1999","unstructured":"I. P. de Guzm\u00e1n, M. Ojeda-Aciego, and A. Valverde. Implicates and reduction techniques for temporal logics. Ann. Math. Artificial Intelligence 27:3\u201323, 1999.","journal-title":"Ann. Math. Artificial Intelligence"},{"key":"13_CR5","unstructured":"I. P. de Guzm\u00e1n, M. Ojeda-Aciego, and A. Valverde. Multiple-valued tableaux with \u0394-reductions. In Proc. of the Intl. Conf. on Artificial Intelligence, ICAI\u201999, pages 177\u2013183. C.S.R.E.A., 1999."},{"key":"13_CR6","unstructured":"J.H. Gallier. Logic for Computer Science: Foundations for Automatic Theorem Proving. Wiley & Sons, 1987."},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"F. Massacci. Simplification: a general constraint propagation technique for propositional and modal tableaux. In Proceedings of Tableaux\u201998, pages 217\u2013231. Lect. Notes in Artificial Intelligence 1397, 1998.","DOI":"10.1007\/3-540-69778-0_24"},{"key":"13_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L.C. Paulson","year":"1994","unstructured":"L.C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828."},{"key":"13_CR9","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0255(94)90032-9","volume":"78","author":"P. W. Purdom Jr.","year":"1994","unstructured":"P. W. Purdom, Jr. Average time for the full pure literal rule. Information Sciences, 78:269\u2013291, 1994.","journal-title":"Information Sciences"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40006-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T23:22:41Z","timestamp":1556752961000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40006-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540411314","9783540400066"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-40006-0_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}