{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,3]],"date-time":"2025-11-03T22:56:16Z","timestamp":1762210576073,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,12,5]],"date-time":"2008-12-05T00:00:00Z","timestamp":1228435200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Resolution refinements called w-resolution trees with lemmas (WRTL) and with\ninput lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both\nWRTL and WRTI when there is no regularity condition. For regular proofs, an\nexponential separation between regular dag-like resolution and both regular\nWRTL and regular WRTI is given.\n  It is proved that DLL proof search algorithms that use clause learning based\non unit propagation can be polynomially simulated by regular WRTI. More\ngenerally, non-greedy DLL algorithms with learning by unit propagation are\nequivalent to regular WRTI. A general form of clause learning, called\nDLL-Learn, is defined that is equivalent to regular WRTL.\n  A variable extension method is used to give simulations of resolution by\nregular WRTI, using a simplified form of proof trace extensions. DLL-Learn and\nnon-greedy DLL algorithms with learning by unit propagation can use variable\nextensions to simulate general resolution without doing restarts.\n  Finally, an exponential lower bound for WRTL where the lemmas are restricted\nto short clauses is shown.<\/jats:p>","DOI":"10.2168\/lmcs-4(4:13)2008","type":"journal-article","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T10:25:32Z","timestamp":1231496732000},"source":"Crossref","is-referenced-by-count":19,"title":["Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning"],"prefix":"10.46298","volume":"Volume 4, Issue 4","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[]},{"given":"Jan","family":"Hoffmann","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Johannsen","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,12,5]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/860\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/860\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:57:59Z","timestamp":1681243079000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/860"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,12,5]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(4:13)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0811.1075","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0811.1075","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,12,5]]},"article-number":"860"}}