Skip to main content
SpringerLink
Log in
Book cover

Methods of Cut-Elimination pp 39–61Cite as

Complexity of Cut-Elimination

  • Chapter
  • First Online:

Part of the book series: Trends in Logic ((TREN,volume 34))

Abstract

Our aim is to compare different methods of cut-elimination. For this aim we need logic-free axioms. The original formulation of LK by Gentzen also served the purpose of simulating Hilbert-type calculi and deriving axiom schemata within fixed proof length. Below we show that there exists a polynomial transformation from an LK-proof with arbitrary axioms of type A ⊢ A to atomic ones.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD   109.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    Note that, in [16] we chose alternative (1).

References

  1. M. Baaz, A. Leitsch: Complexity of Resolution Proofs and Function Introduction. Annals of Pure and Applied Logic, 57, pp. 181–215, 1992.

    Article  MathSciNet  MATH  Google Scholar 

  2. M. Baaz, A. Leitsch: On Skolemization and Proof Complexity. Fundamenta Informaticae, 20(4), pp. 353–379, 1994.

    MathSciNet  MATH  Google Scholar 

  3. W.S. Brianerd, L.H. Landweber: Theory of Computation. Wiley, New York, NY, 1974.

    Google Scholar 

  4. G. Gentzen: Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, pp. 405–431, 1934–1935.

    Article  MathSciNet  Google Scholar 

  5. J. Herbrand: Sur le problème fondamental de la logique mathématique. Sprawozdania z posiedzen Towarzysta Naukowego Warszawskiego, Wydzial III, 24, pp. 12–56, 1931.

    Google Scholar 

  6. V.P. Orevkov: Lower Bounds for Increasing Complexity of Derivations after Cut Elimination. Journal of Soviet Mathematics, 20, pp. 2337–2350, 1982.

    Article  MATH  Google Scholar 

  7. P. Pudlak: The Lengths of Proofs. In: S.R. Buss (ed.), Handbook of Proof Theory, Elsevier, Amsterdam, 1998.

    Google Scholar 

  8. R. Statman: Lower Bounds on Herbrand’s Theorem. Proceedings of the American Mathematical Society 75, pp. 104–107, 1979.

    MathSciNet  MATH  Google Scholar 

  9. G. Takeuti: Proof Theory. North-Holland, Amsterdam, 2nd edition, 1987.

    Google Scholar 

  10. B. Woltzenlogel Paleo: Herbrand Sequent Extraction. VDM Verlag Dr.Müller e.K., Saarbrücken, , ISBN-10: 3836461528, February 7, 2008.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Vienna University of Technology, Wiedner Hauptstraße 8-10, 1040, Vienna, Austria

    Matthias Baaz

  2. Vienna University of Technology, Favoritenstraße 9, 1040, Vienna, Austria

    Alexander Leitsch

Authors
  1. Matthias Baaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alexander Leitsch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthias Baaz .

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer Science+Business Media B.V.

About this chapter

Cite this chapter

Baaz, M., Leitsch, A. (2011). Complexity of Cut-Elimination. In: Methods of Cut-Elimination. Trends in Logic, vol 34. Springer, Dordrecht. https://doi.org/10.1007/978-94-007-0320-9_4

Download citation

Publish with us

Policies and ethics

Search

Navigation