{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:20Z","timestamp":1753894400791,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We pioneer a new technique that allows us to prove a multitude of previously\nopen simulations in QBF proof complexity. In particular, we show that extended\nQBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus,\nLong-Distance Q-Resolution, and Merge Resolution. These results are obtained by\ntaking a technique of Beyersdorff et al. (JACM 2020) that turns strategy\nextraction into simulation and combining it with new local strategy extraction\narguments.\n  This approach leads to simulations that are carried out mainly in\npropositional logic, with minimal use of the QBF rules. Our proofs therefore\nprovide a new, largely propositional interpretation of the simulated systems.\nWe argue that these results strengthen the case for uniform certification in\nQBF solving, since many QBF proof systems now fall into place underneath\nextended QBF Frege.<\/jats:p>","DOI":"10.46298\/lmcs-20(1:14)2024","type":"journal-article","created":{"date-parts":[[2024,2,13]],"date-time":"2024-02-13T10:40:05Z","timestamp":1707820805000},"source":"Crossref","is-referenced-by-count":0,"title":["Towards Uniform Certification in QBF"],"prefix":"10.46298","volume":"Volume 20, Issue 1","author":[{"given":"Leroy","family":"Chew","sequence":"first","affiliation":[]},{"given":"Friedrich","family":"Slivovsky","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,2,13]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/13049\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/13049\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,13]],"date-time":"2024-02-13T10:40:06Z","timestamp":1707820806000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/10146"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,2,13]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(1:14)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2210.07085v2","asserted-by":"subject"},{"id-type":"arxiv","id":"2210.07085v1","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2210.07085","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2210.07085","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,2,13]]},"article-number":"10146"}}