{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T10:18:49Z","timestamp":1725617929177},"reference-count":24,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2020,1,25]],"date-time":"2020-01-25T00:00:00Z","timestamp":1579910400000},"content-version":"vor","delay-in-days":1485,"URL":"http:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["239962"],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2016,1]]},"DOI":"10.1016\/j.tcs.2015.10.020","type":"journal-article","created":{"date-parts":[[2015,10,24]],"date-time":"2015-10-24T18:06:05Z","timestamp":1445709965000},"page":"83-101","update-policy":"http:\/\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":25,"special_numbering":"C","title":["Soundness of Q-resolution with dependency schemes"],"prefix":"10.1016","volume":"612","author":[{"given":"Friedrich","family":"Slivovsky","sequence":"first","affiliation":[]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/j.tcs.2015.10.020_br0010","doi-asserted-by":"crossref","first-page":"86","DOI":"10.1016\/j.tcs.2013.12.020","article-title":"Henkin quantifiers and Boolean formulae: a certification perspective of DQBF","volume":"523","author":"Balabanov","year":"2014","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"10.1016\/j.tcs.2015.10.020_br0020","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s10703-012-0152-6","article-title":"Unified QBF certification and its applications","volume":"41","author":"Balabanov","year":"2012","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.tcs.2015.10.020_br0030","series-title":"Tools and Algorithms for Construction and Analysis of Systems, Proceedings of the 5th International Conference, TACAS '99, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'99","first-page":"193","article-title":"Symbolic model checking without BDDs","volume":"vol. 1579","author":"Biere","year":"1999"},{"key":"10.1016\/j.tcs.2015.10.020_br0040","series-title":"Theory and Applications of Satisfiability Testing","first-page":"158","article-title":"Integrating dependency schemes in search-based QBF solvers","volume":"vol. 6175","author":"Biere","year":"2010"},{"key":"10.1016\/j.tcs.2015.10.020_br0050","series-title":"Computer Aided Verification, Proceedings of the 13th International Conference","first-page":"454","article-title":"Finding bugs in an alpha microprocessor using satisfiability solvers","author":"Bjesse","year":"2001"},{"key":"10.1016\/j.tcs.2015.10.020_br0060","article-title":"Model-Based Transformations for Quantified Boolean Formulas","volume":"vol. 329","author":"Bubeck","year":"2010"},{"issue":"1","key":"10.1016\/j.tcs.2015.10.020_br0070","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","article-title":"Resolution for quantified Boolean formulas","volume":"117","author":"B\u00fcning","year":"1995","journal-title":"Inform. and Comput."},{"issue":"2","key":"10.1016\/j.tcs.2015.10.020_br0080","doi-asserted-by":"crossref","DOI":"10.1023\/A:1015019416843","article-title":"An algorithm to evaluate quantified Boolean formulae and its experimental evaluation","volume":"28","author":"Cadoli","year":"2002","journal-title":"J. Automat. Reason."},{"key":"10.1016\/j.tcs.2015.10.020_br0090","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1145\/368273.368557","article-title":"A machine program for theorem-proving","volume":"5","author":"Davis","year":"1962","journal-title":"Commun. ACM"},{"key":"10.1016\/j.tcs.2015.10.020_br0100","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","article-title":"Clause\/term resolution and learning in the evaluation of quantified Boolean formulas","volume":"26","author":"Giunchiglia","year":"2006","journal-title":"J. Artificial Intelligence Res."},{"key":"10.1016\/j.tcs.2015.10.020_br0110","series-title":"Proceedings of IJCAI 2011","first-page":"546","article-title":"A uniform approach for generating proofs and strategies for both true and false QBF formulas","author":"Goultiaeva","year":"2011"},{"key":"10.1016\/j.tcs.2015.10.020_br0120","series-title":"Automated Reasoning, 7th International Joint Conference","first-page":"91","article-title":"A unified proof system for QBF preprocessing","volume":"vol. 8562","author":"Heule","year":"2014"},{"key":"10.1016\/j.tcs.2015.10.020_br0130","article-title":"On unification of QBF resolution-based calculi","author":"Janota","year":"2014","journal-title":"Electron. Colloq. Comput. Complex."},{"key":"10.1016\/j.tcs.2015.10.020_br0140","series-title":"Theory and Applications of Satisfiability Testing","first-page":"67","article-title":"On propositional QBF expansions and Q-resolution","volume":"vol. 7962","author":"Janota","year":"2013"},{"key":"10.1016\/j.tcs.2015.10.020_br0150","series-title":"Proceedings of the Thirteenth AAAI Conference on Artificial Intelligence","first-page":"1194","article-title":"Pushing the envelope: planning, propositional logic, and stochastic search","author":"Kautz","year":"1996"},{"key":"10.1016\/j.tcs.2015.10.020_br0160","series-title":"Dependency schemes and search-based qbf solving: theory and practice","author":"Lonsing","year":"2012"},{"issue":"2","key":"10.1016\/j.tcs.2015.10.020_br0170","doi-asserted-by":"crossref","first-page":"156","DOI":"10.1007\/s10009-004-0183-4","article-title":"A survey of recent advances in SAT-based formal verification","volume":"7","author":"Prasad","year":"2005","journal-title":"Softw. Tools Technol. Transf."},{"key":"10.1016\/j.tcs.2015.10.020_br0180","series-title":"Theory and Applications of Satisfiability Testing","first-page":"430","article-title":"Resolution-based certificate extraction for QBF","volume":"vol. 7317","author":"Niemetz","year":"2012"},{"issue":"78","key":"10.1016\/j.tcs.2015.10.020_br0190","doi-asserted-by":"crossref","first-page":"957","DOI":"10.1016\/S0898-1221(00)00333-3","article-title":"Lower bounds for multiplayer noncooperative games of incomplete information","volume":"41","author":"Peterson","year":"2001","journal-title":"Comput. Math. Appl."},{"key":"10.1016\/j.tcs.2015.10.020_br0200","series-title":"Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings of the 15th International Conference","first-page":"512","article-title":"Variable dependencies of quantified CSPs","volume":"vol. 5330","author":"Samer","year":"2008"},{"issue":"1","key":"10.1016\/j.tcs.2015.10.020_br0210","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/s10817-008-9114-5","article-title":"Backdoor sets of quantified Boolean formulas","volume":"42","author":"Samer","year":"2009","journal-title":"J. Automat. Reason."},{"key":"10.1016\/j.tcs.2015.10.020_br0220","series-title":"Progress in Artificial Intelligence, 9th Portuguese Conference on Artificial Intelligence","first-page":"62","article-title":"The impact of branching heuristics in propositional satisfiability algorithms","volume":"vol. 1695","author":"Silva","year":"1999"},{"key":"10.1016\/j.tcs.2015.10.020_br0230","series-title":"Theory and Applications of Satisfiability Testing","first-page":"58","article-title":"Computing resolution-path dependencies in linear time","volume":"vol. 7317","author":"Slivovsky","year":"2012"},{"key":"10.1016\/j.tcs.2015.10.020_br0240","series-title":"Principles and Practice of Constraint Programming","first-page":"789","article-title":"Variable independence and resolution paths for quantified Boolean formulas","volume":"vol. 6876","author":"Van Gelder","year":"2011"}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397515009135?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397515009135?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,1,25]],"date-time":"2020-01-25T02:05:25Z","timestamp":1579917925000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397515009135"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1]]},"references-count":24,"alternative-id":["S0304397515009135"],"URL":"https:\/\/doi.org\/10.1016\/j.tcs.2015.10.020","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2016,1]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"Soundness of Q-resolution with dependency schemes","name":"articletitle","label":"Article Title"},{"value":"Theoretical Computer Science","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.tcs.2015.10.020","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2015 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}