On Generalizations of Semi-terms of Particularly Simple Form | SpringerLink
Skip to main content
Springer Nature Link
Log in

On Generalizations of Semi-terms of Particularly Simple Form

  • Conference paper
  • First Online:
Computer Science Logic (CSL 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2471))

Included in the following conference series:

  • 543 Accesses

Abstract

We show that Gentzen’s sequent calculus admits generalization of semi-terms of particularly simple form. This theorem extends one of the main results in [BS95] to languages \( \mathcal{L} \) with functions of arbitrary arity and the central result in [KP88] to semi-terms.

The work on this paper was partly sponsored by FWF grant P15477-MAT.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 11439
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 14299
Price includes VAT (Japan)
  • Compact, lightweight 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. M. Baaz and G. Moser. Herbrand’s Theorem and Term Induction. Submitted to the Annals of Pure and Applied Logic, 2001.

    Google Scholar 

  2. M. Baaz and P. Pudlák. Kreisel’s conjecture for L∃1. In P. Clote and J. Krajíćek, editors, Arithmetic, Proof Theory and Computational Complexity, pages 29–59. Oxford University, 1993. With a postscript by G. Kreisel.

    Google Scholar 

  3. M. Baaz and G. Salzer. Semi-unification and geralization of a particularyly simply form. In L. Pacholski and J. Tiuryn, editors, Proc. 8 th Workshop CSL’94, volume LNCS 933, pages 106–120. Springer Verlag, 1995.

    Google Scholar 

  4. F. Baader and W. Snyder. Unification theory. In A. Voronkov, editor, Handbook of Automated Reasoning, volume I, pages 445–532. 2001.

    Google Scholar 

  5. S. R. Buss. An Introduction to Proof Theory. In S. R. Buss, editor, Handbook of Proof Theory, pages 1–79. Elsevier Science, 1998.

    Google Scholar 

  6. Baaz and P. Wojtilak. Generalizing Proofs in Monadic languages. With a postscript by G. Kreisel. Submitted to the Annals of Pure and Applied Logic, 2001.

    Google Scholar 

  7. M. Baaz and R. Zach. Generalizing theorems in real closed fields. Ann. of Pure and Applied Logics, 75:3–23, 1995.

    Article  MATH  MathSciNet  Google Scholar 

  8. C.-L. Chang and R. C. T. Lee. Symbolic Logic an Mechanical Theorem Proving. Academic Press, New York, 1973.

    Google Scholar 

  9. G. Gentzen. Untersuchungen über das logische Schlieβen I—II. Math. Zeitschrift, 39:176–210, 405–431, 1934.

    Article  MATH  MathSciNet  Google Scholar 

  10. J. Krajíćek and P. Pudlák. The number of proof lines and the size of proofs in first-order logic. Arch. Math. Logic, 27:69–84, 1988.

    Article  MATH  MathSciNet  Google Scholar 

  11. G. Moser. Term Induction. PhD thesis, Vienna University of Technology, June 2001.

    Google Scholar 

  12. R. J. Parikh. Some results on the length of proofs. Trans. Amer. Math. Soc. pages 29–36, 1973.

    Google Scholar 

  13. P. Pudlak. The Lengths of Proofs. In S. Buss, editor, Handbook of Proof Theory, pages 547–639. Elsevier, 1998.

    Google Scholar 

  14. C. Weidenbach. Unification in Pseudo-Linear Sort Theories is Decidable. In 13th International Conference on Automated Deduction, CADE-13, LNCS. Springer, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Algebra und Computermathematik, Vienna University of Technology, E118.2, Wiedner Hauptstrasse 8-10, A-1040, Vienna

    Matthias Baaz & Georg Moser

Authors
  1. Matthias Baaz
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Georg Moser
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Laboratory for Foundations of Computer Science Division of Informatics, University of Edinburgh, King’s Buildings, Mayfield Road, Edinburgh, EH9 3JZ, UK

    Julian Bradfield

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baaz, M., Moser, G. (2002). On Generalizations of Semi-terms of Particularly Simple Form. In: Bradfield, J. (eds) Computer Science Logic. CSL 2002. Lecture Notes in Computer Science, vol 2471. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45793-3_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-45793-3_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-44240-0

  • Online ISBN: 978-3-540-45793-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation