A non-elementary speed-up in proof length by structural clause form transformation
Matthias Baaz, Christian G. Fermüller, Alexander Leitsch · 2002
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 formulassuch 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.>