Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

STOC

1999

ACM

1999

ACM

The width of a Resolution proof is defined to be the maximal number of literals in any clause of the proof. In this paper, we relate proof width to proof length (ϭsize), in both general Resolution, and its tree-like variant. The following consequences of these relations reveal width as a crucial “resource” of Resolution proofs. In one direction, the relations allow us to give simple, unified proofs for almost all known exponential lower bounds on size of resolution proofs, as well as several interesting new ones. They all follow from width lower bounds, and we show how these follow from natural expansion property of clauses of the input tautology. In the other direction, the width-size relations naturally suggest a simple dynamic programming procedure for automated theorem proving—one which simply searches for small width proofs. This relation guarantees that the running time (and thus the size of the produced proof) is at most quasi-polynomial in the smallest tree-like proof. T...

Added |
03 Aug 2010 |

Updated |
03 Aug 2010 |

Type |
Conference |

Year |
1999 |

Where |
STOC |

Authors |
Eli Ben-Sasson, Avi Wigderson |

Comments (0)