{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,11]],"date-time":"2026-03-11T16:57:15Z","timestamp":1773248235868,"version":"3.50.1"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,4,17]],"date-time":"2012-04-17T00:00:00Z","timestamp":1334620800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2012,8]]},"DOI":"10.1007\/s10703-012-0152-6","type":"journal-article","created":{"date-parts":[[2012,4,16]],"date-time":"2012-04-16T09:38:37Z","timestamp":1334569117000},"page":"45-65","source":"Crossref","is-referenced-by-count":96,"title":["Unified QBF certification and its applications"],"prefix":"10.1007","volume":"41","author":[{"given":"Valeriy","family":"Balabanov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jie-Hong R.","family":"Jiang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,4,17]]},"reference":[{"key":"152_CR1","volume-title":"Proc int\u2019l conf on logic for programming, artificial intelligence and reasoning (LPAR)","author":"M Benedetti","year":"2004","unstructured":"Benedetti M (2004) Evaluating QBFs via symbolic skolemization. In: Proc int\u2019l conf on logic for programming, artificial intelligence and reasoning (LPAR)"},{"key":"152_CR2","volume-title":"Proc int\u2019l joint conf on artificial intelligence (IJCAI)","author":"M Benedetti","year":"2005","unstructured":"Benedetti M (2005) Extracting certificates from quantified Boolean formulas. In: Proc int\u2019l joint conf on artificial intelligence (IJCAI)"},{"key":"152_CR3","volume-title":"Proc. design automation and test in Europe","author":"R Bloem","year":"2007","unstructured":"Bloem R, Galler S, Jobstmann B, Piterman N, Pnueli A, Weiglhofer M (2007) Automatic hardware synthesis from specifications: a\u00a0case study. In: Proc. design automation and test in Europe (DATE)"},{"key":"152_CR4","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1007\/978-3-642-22110-1_12","volume-title":"Proc int\u2019l conf on computer aided verification (CAV)","author":"V Balabanov","year":"2011","unstructured":"Balabanov V, Jiang J-HR (2011) Resolution proofs and Skolem functions in QBF evaluation and applications. In: Proc int\u2019l conf on computer aided verification (CAV), pp 149\u2013164"},{"key":"152_CR5","unstructured":"Berkeley Logic Synthesis and Verification Group. ABC: a\u00a0system for sequential synthesis and verification. http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"issue":"2","key":"152_CR6","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/A:1015019416843","volume":"28","author":"M Cadoli","year":"2002","unstructured":"Cadoli M, Schaerf M, Giovanardi A, Giovanardi M (2002) An algorithm to evaluate quantified Boolean formulae and its experimental evaluation. J Autom Reason 28(2):101\u2013142","journal-title":"J Autom Reason"},{"key":"152_CR7","volume-title":"Proc int\u2019l conf on theory and applications of satisfiability testing (SAT)","author":"N Dershowitz","year":"2005","unstructured":"Dershowitz N, Hanna Z, Katz J (2005) Bounded model checking with QBF. In: Proc int\u2019l conf on theory and applications of satisfiability testing (SAT)"},{"key":"152_CR8","first-page":"502","volume-title":"Proc int\u2019l conf on theory and applications of satisfiability testing (SAT)","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) An extensible SAT-solver. In: Proc int\u2019l conf on theory and applications of satisfiability testing (SAT), pp 502\u2013518"},{"key":"152_CR9","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1613\/jair.1959","volume":"26","author":"E Giunchiglia","year":"2006","unstructured":"Giunchiglia E, Narizzano M, Tacchella A (2006) Clause-term resolution and learning in quantified Boolean logic satisfiability. Artif Intell Res 26:371\u2013416","journal-title":"Artif Intell Res"},{"key":"152_CR10","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-540-72788-0_21","volume-title":"Proc int\u2019l conf on theory and applications of satisfiability testing (SAT)","author":"T Jussila","year":"2007","unstructured":"Jussila T, Biere A, Sinz C, Kr\u00f6ning D, Wintersteiger C (2007) A first step towards a unified proof checker for QBF. In: Proc int\u2019l conf on theory and applications of satisfiability testing (SAT), pp 201\u2013214"},{"key":"152_CR11","first-page":"779","volume-title":"Proc int\u2019l conf on computer-aided design (ICCAD)","author":"J-HR Jiang","year":"2009","unstructured":"Jiang J-HR, Lin H-P, Hung W-L (2009) Interpolating functions from large Boolean relations. In: Proc int\u2019l conf on computer-aided design (ICCAD), pp 779\u2013784"},{"issue":"1","key":"152_CR12","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1006\/inco.1995.1025","volume":"117","author":"H Kleine-B\u00fcning","year":"1995","unstructured":"Kleine-B\u00fcning H, Karpinski M, Fl\u00f6gel A (1995) Resolution for quantified Boolean formulas. Inf Comput 117(1):12\u201318","journal-title":"Inf Comput"},{"key":"152_CR13","volume-title":"AI communications","author":"M Narizzano","year":"2009","unstructured":"Narizzano M, Peschiera C, Pulina L, Tacchella A (2009) Evaluating and certifying QBFs: a\u00a0comparison of state-of-the-art tools. In: AI communications"},{"key":"152_CR14","volume-title":"Computational complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou CH (1994) Computational complexity. Addison-Wesley, Reading"},{"key":"152_CR15","unstructured":"QBF solver evaluation portal. http:\/\/www.qbflib.org\/qbfeval\/"},{"key":"152_CR16","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1613\/jair.591","volume":"10","author":"J Rintanen","year":"1999","unstructured":"Rintanen J (1999) Constructing conditional plans by a theorem-prover. J Artif Intell Res 10:323\u2013352","journal-title":"J Artif Intell Res"},{"key":"152_CR17","first-page":"125","volume":"10","author":"Th Skolem","year":"1928","unstructured":"Skolem Th (1928) \u00dcber die Mathematische Logik. Nor Mat Tidsskr 10:125\u2013142 [Translation in From Frege to G\u00f6del, a\u00a0source book in mathematical logic, J van Heijenoort, Harvard Univ Press, 1967]","journal-title":"Nor Mat Tidsskr"},{"key":"152_CR18","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Proc. int\u2019l conf. on theory and applications of satisfiability testing (SAT)","author":"S Staber","year":"2007","unstructured":"Staber S, Bloem R (2007) Fault localization and correction with QBF. In: Proc. int\u2019l conf. on theory and applications of satisfiability testing (SAT), pp 355\u2013368"},{"key":"152_CR19","doi-asserted-by":"crossref","first-page":"404","DOI":"10.1145\/1168857.1168907","volume-title":"Proc int\u2019l conf on architectural support for programming languages and operating systems (ASPLOS)","author":"A Solar-Lezama","year":"2006","unstructured":"Solar-Lezama A, Tancau L, Bod\u00edk R, Seshia S, Saraswat V (2006) Combinatorial sketching for finite programs. In: Proc int\u2019l conf on architectural support for programming languages and operating systems (ASPLOS), pp 404\u2013415"},{"key":"152_CR20","first-page":"466","volume-title":"Studies in constructive mathematics and mathematical logic","author":"G Tseitin","year":"1970","unstructured":"Tseitin G (1970) On the complexity of derivation in propositional calculus. In: Studies in constructive mathematics and mathematical logic, pp 466\u2013483"},{"key":"152_CR21","volume-title":"Proc Asia and South Pacific design automation conference (ASP-DAC)","author":"Y Yu","year":"2005","unstructured":"Yu Y, Malik S (2005) Validating the result of a quantified Boolean formula (QBF) solvers: theory and practice. In: Proc Asia and South Pacific design automation conference (ASP-DAC)"},{"key":"152_CR22","first-page":"442","volume-title":"Proc int\u2019l conf on computer-aided design (ICCAD)","author":"L Zhang","year":"2002","unstructured":"Zhang L, Malik S (2002) Conflict driven learning in a quantified Boolean satisfiability solver. In: Proc int\u2019l conf on computer-aided design (ICCAD), pp 442\u2013449"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0152-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0152-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0152-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,27]],"date-time":"2019-06-27T10:24:37Z","timestamp":1561631077000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0152-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,17]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,8]]}},"alternative-id":["152"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0152-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,4,17]]}}}