학술논문
A non-elementary speed-up in proof length by structural clause form transformation
Document Type
Conference
Author
Source
Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science Logic in computer science Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on. :213-219 1994
Subject
Language
Abstract
We investigate the effects of different types of translations of first-order formulas to clausal form on minimal proof length. We show that there is a sequence of unsatisfiable formulas such that the length of all refutations of non-structural clause forms of F/sub n/ is non-elementary (in the size of F/sub n/), but there are refutations of structural clause forms of F/sub n/ that are of elementary (at most triple exponential) length.ETX