Skip to main content
SpringerLink
Log in

Program Development by Proof Transformation

  • Conference paper
Proof and Computation

Part of the book series: NATO ASI Series ((NATO ASI F,volume 139))

Abstract

We begin by reviewing the natural deduction rules for the →∧∀-fragment of minimal logic. It is shown how intuitionistic and classical logic can be embedded. Recursion and induction is added to obtain a more realistic proof system. Simple types are added in order to make the language more expressive. We also consider two alternative methods to deal with the strong or constructive existential quantifier ∃*. Finally we discuss the well-known notion of an extracted program of a derivation involving ∃*, in order to set up a relation between the two alternatives.

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

Access this chapter

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 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

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.

References

  1. Ulrich Berger. Program extraction from normalization proofs. In M. Bezem and J.F. Groote, editors, Typed Lambda Calculi and Applications, pages 91–106. Springer Lecture Notes in Computer Science Vol. 664, 1993.

    Chapter  Google Scholar 

  2. Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57: 793–807, 1992.

    MathSciNet  Google Scholar 

  3. Harvey Friedman. Classically and intuitionistically provably recursive functions. In Dana S. Scott and Gert H. Müller, editors, Higher Set Theory, pages 21–28. Springer Lecture Notes in Mathematics, Volume 699, 1978.

    Chapter  Google Scholar 

  4. Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1934.

    Article  MathSciNet  Google Scholar 

  5. Christopher Alan Goad. Computational uses of the manipulation of formal proofs. PhD thesis, Stanford University, August 1980. Stanford Department of Computer Science Report No. STAN-CS-80-819.

    Google Scholar 

  6. Jörg Hudelmaier. Bounds for cut elimination in intuitionistic propositional logic. Archive for Mathematical Logic, 31: 331–354, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  7. Dale Miller. A logic programming language with lambda-abstraction, function variables and simple unification. Journal of Logic and Computation, 2 (4): 497–536, 1991.

    Article  Google Scholar 

  8. G.E. Mints. On e-theorems (in russian). Zapiski, 40: 110–118, 1974.

    MATH  Google Scholar 

  9. Chetan Murthy. Extracting constructive content from classical proofs. Technical Report 90-1151, Dep. of Comp.Science, Cornell Univ., Ithaca, New York, 1990. PhD thesis.

    Google Scholar 

  10. Tobias Nipkow. Functional unification of higher-order patterns. In Proc. 8th IEEE Symp. Logic in Computer Science, pages 64–74, 1993.

    Google Scholar 

  11. Dag Prawitz. Natural Deduction, volume 3 of Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy. Almqvist amp; Wiksell, Stockholm, 1965.

    Google Scholar 

  12. Dan Sahlin, Torkel Franzen, and Seif Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2 (6): 619–656, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  13. Helmut Schwichtenberg. Proofs as programs. In Peter Aczel, Harold Simmons, and Stanley S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 81–113. Cambridge University Press, 1992.

    Google Scholar 

  14. N. Shankar. Proof search in intuitionistic sequent calculus, 1991.

    Google Scholar 

  15. Wilfried Sieg and Richard Scheines. Searching for proofs (in sentential logic). In Leslie Burkholder, editor, Philosophy and the computer, pages 137–159, Boulder, San Francisco, Oxford, 1992. Westview Press.

    Google Scholar 

  16. Martin Stein. Interpretationen der Heyting-Arithmetik endlicher Typen. PhD thesis, Universität Münster, Fachbereich Mathematik, 1976.

    Google Scholar 

  17. Anne S. Troelstra, editor. Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, volume 344 of Lecture Notes in Mathematics. Springer, Berlin, 1973.

    Google Scholar 

  18. Anne S. Troelstra and Dirk van Dalen. Constructivism in Mathematics. An Introduction, volume 121,123 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1988.

    Google Scholar 

  19. Anton Wallner. Komplexe Existenzbeweise in der Arithmetik. Master’s thesis, Mathematisches Institut der Universität München, 1993.

    Google Scholar 

  20. Hermann Weyl. Uber die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10, 1921.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Mathematisches Institut, der Universität München, Theresienstraße 39, D-80333, München, Germany

    Ulrich Berger & Helmut Schwichtenberg

Authors
  1. Ulrich Berger
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Helmut Schwichtenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Mathematisches Institut, Ludwig-Maximilians-Universität München, Theresienstraße 39, D-80333, München, Germany

    Helmut Schwichtenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Berger, U., Schwichtenberg, H. (1995). Program Development by Proof Transformation. In: Schwichtenberg, H. (eds) Proof and Computation. NATO ASI Series, vol 139. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-79361-5_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-79361-5_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-79363-9

  • Online ISBN: 978-3-642-79361-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation