• DocumentCode
    1996321
  • Title

    A non-elementary speed-up in proof length by structural clause form transformation

  • Author

    Baaz, Matthias ; Fermüller, Christian G. ; Leitsch, Alexander

  • Author_Institution
    Inst. fur Algebra und Diskrete Math., Tech. Univ. Wien, Austria
  • fYear
    1994
  • fDate
    4-7 Jul 1994
  • Firstpage
    213
  • Lastpage
    219
  • 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 ⟨Fn⟩ such that the length of all refutations of non-structural clause forms of Fn is non-elementary (in the size of Fn), but there are refutations of structural clause forms of Fn that are of elementary (at most triple exponential) length
  • Keywords
    formal logic; theorem proving; first-order formulas; minimal proof length; nonelementary speed-up; proof length; refutations; structural clause form transformation; structural clause forms; unsatisfiable formulas; Algebra; Calculus;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 1994. LICS '94. Proceedings., Symposium on
  • Conference_Location
    Paris
  • Print_ISBN
    0-8186-6310-3
  • Type

    conf

  • DOI
    10.1109/LICS.1994.316070
  • Filename
    316070
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1996321