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

**Matthias Baaz Christian G. Fermüller 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{BaazFermllerLeitsch-Anonelementaryspeed, author = {Matthias Baaz and Christian G. Fermüller and Alexander Leitsch}, title = {A non-elementary speed-up in proof length by structural clause form transformation }, booktitle = {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)}, year = {1994}, month = {July}, pages = {213--219}, location = {Paris, France}, publisher = {IEEE Computer Society Press} }