## Paper: A non-elementary speed-up in proof length by structural clause form transformation (at LICS 1994)

Authors:**Matthias Baaz Christian Fermuller Alexander Leitsch**

### 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 〈F_{n}〉 such that the length of all refutations of non-structural clause forms of F_{n} is non-elementary (in the size of F_{n}), but there are refutations of structural clause forms of F_{n} that are of elementary (at most triple exponential) length

### BibTeX

@InProceedings{BaazFermullerLeitsc-Anonelementaryspeed, author = {Matthias Baaz and Christian Fermuller and Alexander Leitsch}, title = {A non-elementary speed-up in proof length by structural clause form transformation }, booktitle = {Proceedings of the Ninth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1994}, year = 1994, editor = {Samson Abramsky}, month = {July}, pages = {213--219}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }