{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T14:10:14Z","timestamp":1781014214529,"version":"3.54.1"},"reference-count":13,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2007,4,14]],"date-time":"2007-04-14T00:00:00Z","timestamp":1176508800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2007,4,14]],"date-time":"2007-04-14T00:00:00Z","timestamp":1176508800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,7]]},"DOI":"10.1007\/s10817-007-9067-0","type":"journal-article","created":{"date-parts":[[2007,4,18]],"date-time":"2007-04-18T17:47:28Z","timestamp":1176918448000},"page":"49-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Boolean Functions as Models for Quantified Boolean Formulas"],"prefix":"10.1007","volume":"39","author":[{"given":"Hans","family":"Kleine B\u00fcning","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"K.","family":"Subramani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xishun","family":"Zhao","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2007,4,14]]},"reference":[{"key":"9067_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B. Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M.F., Tarjan, R.E.: A Linear-time algorithm for testing the truth of certain quantified Boolean formulas. Inf. Process. Lett. 8, 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9067_CR2","unstructured":"Cadoli, M., Schaerf, M., Giovanardi, A., Giovanardi, M.: An algorithm to evaluate quantified Boolean formulas and its evaluation. In: Highlights of Satisfiability Research in the Year 2000. IOS, Amsterdam (2000)"},{"key":"9067_CR3","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"A. Fl\u00f6gel","year":"1995","unstructured":"Fl\u00f6gel, A., Karpinski, M., Kleine B\u00fcning, H.: Resolution for quantified Boolean formulas. Information and Computation. 117, 12\u201318 (1995)","journal-title":"Information and Computation."},{"key":"9067_CR4","unstructured":"Feldmann, R., Monien, B., Schambergers, S.: A distributed algorithm to evaluate quantified Boolean formulas. In: Proceedings of AAAI (2000)"},{"key":"9067_CR5","volume-title":"Computers and Intractability: A Guide to the Theory of NP-Completeness","author":"M.R. Garey","year":"1979","unstructured":"Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. Freeman, San Francisco (1979)"},{"key":"9067_CR6","doi-asserted-by":"crossref","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: a system for deciding quantified Boolean formulas. In: Proceedings of IJCAR, Siena (2001)","DOI":"10.1007\/3-540-45744-5_27"},{"key":"9067_CR7","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A. Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comp. Sci. 39, 297\u2013308 (1985)","journal-title":"Theor. Comp. Sci."},{"key":"9067_CR8","volume-title":"Propositional Logic: Deduction and Algorithms","author":"H. Kleine B\u00fcning","year":"1999","unstructured":"Kleine B\u00fcning, H., Lettmann, T.: Propositional Logic: Deduction and Algorithms. Cambridge University Press, Cambridge (1999)"},{"key":"9067_CR9","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-24605-3_8","volume":"2919","author":"H. Kleine B\u00fcning","year":"2004","unstructured":"Kleine B\u00fcning, H., Subramani, K., Zhao, X.: On Boolean models for quantified Boolean horn formulas. SAT 2003, Italy. Lect. Notes Comput. Sci. 2919, 93\u2013104 (2004)","journal-title":"Italy. Lect. Notes Comput. Sci."},{"key":"9067_CR10","doi-asserted-by":"crossref","unstructured":"Letz, R.: Advances in decision procedure for quantified Boolean formulas. In: Proceedings of IJCAR, Siena (2001)","DOI":"10.1007\/3-540-45616-3_12"},{"key":"9067_CR11","volume-title":"Computational Complexity","author":"C.H. Papadimitriou","year":"1994","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"9067_CR12","unstructured":"Rintanen, J.T.: Improvements to the evaluation of quantified Boolean formulae. In: Proceedings of IJCAI (1999)"},{"key":"9067_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"L.J. Stockmeyer","year":"1977","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comp. Sci. 3, 1\u201322 (1977)","journal-title":"Theor. Comp. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9067-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-007-9067-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9067-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-007-9067-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,5,18]],"date-time":"2022-05-18T07:52:51Z","timestamp":1652860371000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-007-9067-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,4,14]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,7]]}},"alternative-id":["9067"],"URL":"https:\/\/doi.org\/10.1007\/s10817-007-9067-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,4,14]]},"assertion":[{"value":"1 April 2004","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"1 January 2007","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 April 2007","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}