Buss, Samuel R. and Kolodziejczyk, Leszek Aleksander - Small Stone in Pool

lmcs:852 - Logical Methods in Computer Science, June 27, 2014, Volume 10, Issue 2
Small Stone in Pool

Authors: Buss, Samuel R. and Kolodziejczyk, Leszek Aleksander

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 (regRTI). Therefore, the Stone tautologies do not separate resolution from DPLL with clause learning.


Source : oai:arXiv.org:1405.5626
DOI : 10.2168/LMCS-10(2:16)2014
Volume: Volume 10, Issue 2
Published on: June 27, 2014
Submitted on: October 31, 2012
Keywords: Computer Science - Logic in Computer Science,Mathematics - Logic


Share

Consultation statistics

This page has been seen 72 times.
This article's PDF has been downloaded 16 times.