{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:35:37Z","timestamp":1725561337458},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540208518"},{"type":"electronic","value":"9783540246053"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24605-3_17","type":"book-chapter","created":{"date-parts":[[2010,7,29]],"date-time":"2010-07-29T04:50:35Z","timestamp":1280379035000},"page":"214-228","source":"Crossref","is-referenced-by-count":15,"title":["Comparing Different Prenexing Strategies for Quantified Boolean Formulas"],"prefix":"10.1007","author":[{"given":"Uwe","family":"Egly","sequence":"first","affiliation":[]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]},{"given":"Hans","family":"Tompits","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"Woltran","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Zolda","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-36126-X_12","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Ayari","year":"2002","unstructured":"Ayari, A., Basin, D.: QUBOS: Deciding Quantified Boolean Logic Using Propositional Satisfiability Solvers. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 187\u2013201. Springer, Heidelberg (2002)"},{"key":"17_CR2","doi-asserted-by":"crossref","first-page":"353","DOI":"10.3233\/FI-1994-2044","volume":"20","author":"M. Baaz","year":"1994","unstructured":"Baaz, M., Leitsch, A.: On Skolemization and Proof Complexity. Fundamenta Informaticae\u00a020, 353\u2013379 (1994)","journal-title":"Fundamenta Informaticae"},{"key":"17_CR3","first-page":"169","volume-title":"Proc. IJCAI 2001","author":"M. Cadoli","year":"2001","unstructured":"Cadoli, M., Eiter, T., Gottlob, G.: Complexity of Nested Circumscription and Abnormality Theories. In: Proc. IJCAI 2001, pp. 169\u2013174. Morgan Kaufmann, San Francisco (2001)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1007\/10703163_7","volume-title":"Computer Science Logic","author":"U. Egly","year":"1999","unstructured":"Egly, U.: Quantifiers and the System KE: Some Surprising Results. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol.\u00a01584, pp. 90\u2013104. Springer, Heidelberg (1999)"},{"key":"17_CR5","unstructured":"Egly, U., Eiter, T., Tompits, H., Woltran, S.: Solving Advanced Reasoning Tasks Using Quantified Boolean Formulas. In: Proc. AAAI 2000, pp. 417\u2013422. AAAI\/MIT Press (2000)"},{"key":"17_CR6","unstructured":"Egly, U., Tompits, H., Woltran, S.: On Quantifier Shifting for Quantified Boolean Formulas. In: Proc. SAT 2002 Workshop on Theory and Applications on QBFs, pp. 48\u201361 (2002)"},{"issue":"3","key":"17_CR7","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1006\/jcss.1996.0083","volume":"53","author":"T. Eiter","year":"1996","unstructured":"Eiter, T., Gottlob, G.: The Complexity of Nested Counterfactuals and Iterated Knowledge Base Revisions. Journal of Computer and System Sciences\u00a053(3), 497\u2013512 (1996)","journal-title":"Journal of Computer and System Sciences"},{"key":"17_CR8","unstructured":"Feldmann, R., Monien, B., Schamberger, S.: A Distributed Algorithm to Evaluate Quantified Boolean Formulas. In: Proc. AAAI 2000, pp. 285\u2013290. AAAI\/MIT Press (2000)"},{"key":"17_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-45744-5_27","volume-title":"Automated Reasoning","author":"E. Giunchiglia","year":"2001","unstructured":"Giunchiglia, E., Narizzano, M., Tacchella, A.: QuBE: A System for Deciding Quantified Boolean Formulas Satisfiability. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 364\u2013369. Springer, Heidelberg (2001)"},{"issue":"6","key":"17_CR10","doi-asserted-by":"publisher","first-page":"827","DOI":"10.1093\/jigpal\/3.6.827","volume":"3","author":"J. Goubault","year":"1995","unstructured":"Goubault, J.: A BDD-Based Simplification and Skolemization Procedure. Logic Journal of the IGPL\u00a03(6), 827\u2013855 (1995)","journal-title":"Logic Journal of the IGPL"},{"key":"17_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/3-540-45616-3_12","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"R. Letz","year":"2002","unstructured":"Letz, R.: Lemma and Model Caching in Decision Procedures for Quantified Boolean Formulas. In: Egly, U., Ferm\u00fcller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol.\u00a02381, pp. 160\u2013175. Springer, Heidelberg (2002)"},{"key":"17_CR12","first-page":"417","volume-title":"Proc. KR 1991","author":"B. Nebel","year":"1991","unstructured":"Nebel, B.: Belief Revision and Default Reasoning: Syntax-Based Approaches. In: Proc. KR 1991, pp. 417\u2013428. Morgan Kaufmann, San Francisco (1991)"},{"volume-title":"Computational Complexity","year":"1994","author":"C.H. Papadimitriou","key":"17_CR13","unstructured":"Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)"},{"key":"17_CR14","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J. Rintanen","year":"1999","unstructured":"Rintanen, J.: Constructing Conditional Plans by a Theorem Prover. Journal of Artificial Intelligence Research\u00a010, 323\u2013352 (1999)","journal-title":"Journal of Artificial Intelligence Research"},{"issue":"1","key":"17_CR15","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. Theoretical Computer Science\u00a03(1), 1\u201322 (1977)","journal-title":"Theoretical Computer Science"},{"key":"17_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-46135-3_14","volume-title":"Principles and Practice of Constraint Programming - CP 2002","author":"L. Zhang","year":"2002","unstructured":"Zhang, L., Malik, S.: Towards a Symmetric Treatment of Satisfaction and Conflicts in Quantified Boolean Formula Evaluation. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol.\u00a02470, pp. 200\u2013215. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24605-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,6,9]],"date-time":"2020-06-09T14:56:39Z","timestamp":1591714599000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24605-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540208518","9783540246053"],"references-count":16,"URL":"http:\/\/dx.doi.org\/10.1007\/978-3-540-24605-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}
