Search

• < Previous
• 1
• Next >

---

Small Stone in Pool

Samuel R. Buss ; Leszek Aleksander Kolodziejczyk.

The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas&nbsp;[&hellip;]

---

Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning

Samuel R. Buss ; Jan Hoffmann ; Jan Johannsen.

Resolution refinements called w-resolution trees with lemmas (WRTL) and with input lemmas (WRTI) are introduced. Dag-like resolution is equivalent to both WRTL and WRTI when there is no regularity condition. For regular proofs, an exponential separation between regular dag-like resolution and both&nbsp;[&hellip;]

---