Search


Volume

Author

Year

  • < Previous
  • 1
  • Next >
1 result

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;]
Published on December 5, 2008
Volume 4, Issue 4
  • < Previous
  • 1
  • Next >