• DocumentCode
    2038545
  • Title

    On the Computational Complexity of Cut-Reduction

  • Author

    Aehlig, Klaus ; Beckmann, Arnold

  • Author_Institution
    Dept. of Comput. Sci., Swansea Univ. Singleton Park, Swansea
  • fYear
    2008
  • fDate
    24-27 June 2008
  • Firstpage
    284
  • Lastpage
    293
  • Abstract
    Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.
  • Keywords
    computational complexity; theorem proving; bounded arithmetic; computational complexity; cut-reduction; Arithmetic; Computational complexity; Computer science; Logic; Machinery; Polynomials; Search problems; Writing; Bounded Arithmetic; cut-reduction; proof notations; propositional logic;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Logic in Computer Science, 2008. LICS '08. 23rd Annual IEEE Symposium on
  • Conference_Location
    Pittsburgh, PA
  • ISSN
    1043-6871
  • Print_ISBN
    978-0-7695-3183-0
  • Type

    conf

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