{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T01:17:08Z","timestamp":1725585428750},"publisher-location":"Berlin, Heidelberg","reference-count":14,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642215803"},{"type":"electronic","value":"9783642215810"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21581-0_20","type":"book-chapter","created":{"date-parts":[[2011,6,10]],"date-time":"2011-06-10T13:30:19Z","timestamp":1307712619000},"page":"245-258","source":"Crossref","is-referenced-by-count":0,"title":["Transformations into Normal Forms for Quantified Circuits"],"prefix":"10.1007","author":[{"given":"Hans Kleine","family":"B\u00fcning","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xishun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Uwe","family":"Bubeck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"20_CR1","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF00289267","volume":"15","author":"S. Anderaa","year":"1981","unstructured":"Anderaa, S., B\u00f6rger, E.: The Equivalence of Horn and Network Complexity for Boolean Functions. Acta Informatica\u00a015, 303\u2013307 (1981)","journal-title":"Acta Informatica"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/3-540-63385-5_37","volume-title":"Computational Logic and Proof Theory","author":"B. Borchert","year":"1997","unstructured":"Borchert, B., Stephan, F.: Looking for an Analogue of Rice\u2019s Theorem in Circuit Complexity Theory. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) KGC 1997. LNCS, vol.\u00a01289, pp. 114\u2013127. Springer, Heidelberg (1997)"},{"issue":"10","key":"20_CR3","doi-asserted-by":"publisher","first-page":"1606","DOI":"10.1016\/j.dam.2007.10.005","volume":"156","author":"U. Bubeck","year":"2008","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Models and Quantifier Elimination for Quantified Horn Formulas. Discrete Applied Mathematics\u00a0156(10), 1606\u20131622 (2008)","journal-title":"Discrete Applied Mathematics"},{"key":"20_CR4","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Encoding Nested Boolean Functions as Quantified Boolean Formulas. In: 3rd Guangzhou Symposium on Satisfiability in Logic-based Modeling, Zhuhai, China (2010)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-14186-7_7","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"U. Bubeck","year":"2010","unstructured":"Bubeck, U., Kleine B\u00fcning, H.: Rewriting (Dependency-)Quantified 2-CNF with arbitrary free literals into existential 2-HORN. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 58\u201370. Springer, Heidelberg (2010)"},{"issue":"3","key":"20_CR6","first-page":"119","volume":"28","author":"S. Cook","year":"1999","unstructured":"Cook, S., Soltys, M.: Boolean Programs and Quantified Propositional Proof Systems. The Bulletin of the Section of Logic\u00a028(3), 119\u2013129 (1999)","journal-title":"The Bulletin of the Section of Logic"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/11499107_32","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. Dershowitz","year":"2005","unstructured":"Dershowitz, N., Hanna, Z., Katz, J.: Bounded model checking with QBF. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol.\u00a03569, pp. 408\u2013414. Springer, Heidelberg (2005)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-540-24605-3_17","volume-title":"Theory and Applications of Satisfiability Testing","author":"U. Egly","year":"2004","unstructured":"Egly, U., Seidl, M., Tompits, H., Woltran, S., Zolda, M.: Comparing Different Prenexing Strategies for Quantified Boolean Formulas. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, pp. 214\u2013228. Springer, Heidelberg (2004)"},{"key":"20_CR9","doi-asserted-by":"crossref","first-page":"747","DOI":"10.1109\/DAC.2002.1012722","volume-title":"Proc. 39th Design Automation Conference (DAC 2002)","author":"M. Ganai","year":"2002","unstructured":"Ganai, M., Zhang, L., Ashar, P., Gupta, A., Malik, S.: Combining Strengths of Circuit-based and CNF-based Algorithms for a High-performance SAT Solver. In: Proc. 39th Design Automation Conference (DAC 2002), pp. 747\u2013750. ACM, New York (2002)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-642-14186-7_29","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2010","author":"A. Goultiaeva","year":"2010","unstructured":"Goultiaeva, A., Bacchus, F.: Exploiting circuit representations in QBF solving. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol.\u00a06175, pp. 333\u2013339. Springer, Heidelberg (2010)"},{"key":"20_CR11","first-page":"232","volume-title":"Proc. 38th Design Automation Conference (DAC 2001)","author":"M. Kuehlmann","year":"2001","unstructured":"Kuehlmann, M., Ganai, M., Paruthi, V.: Circuit-based Boolean Reasoning. In: Proc. 38th Design Automation Conference (DAC 2001), pp. 232\u2013237. ACM, New York (2001)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Meyer, A., Stockmeyer, L.: Word Problems Requiring Exponential Time. In: Proc. 5th ACM Symp. on Theory of Computing (STOC 1973), pp. 1\u20139 (1973)","DOI":"10.1145\/800125.804029"},{"key":"20_CR13","doi-asserted-by":"crossref","unstructured":"Pigorsch, F., Scholl, C.: Exploiting Structure in an AIG based QBF Solver. In: Proc. Intl. Conf. on Design, Automation and Test in Europe (DATE 2009), pp. 1596\u20131601 (2009)","DOI":"10.1109\/DATE.2009.5090919"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/10722167_13","volume-title":"Computer Aided Verification","author":"P. Williams","year":"2000","unstructured":"Williams, P., Biere, A., Clarke, E., Gupta, A.: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 124\u2013138. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing - SAT 2011"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21581-0_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,24]],"date-time":"2021-11-24T23:14:18Z","timestamp":1637795658000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21581-0_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642215803","9783642215810"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21581-0_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}