Program Development by Proof Transformation

  • Ulrich Berger
  • Helmut Schwichtenberg
Part of the NATO ASI Series book series (volume 139)


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.


Derivation Term Atomic Formula Intuitionistic Logic Relation Symbol Assumption Variable 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [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.CrossRefGoogle Scholar
  2. [2]
    Roy Dyckhoff. Contraction-free sequent calculi for intuitionistic logic. Journal of Symbolic Logic, 57: 793–807, 1992.MathSciNetGoogle Scholar
  3. [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.CrossRefGoogle Scholar
  4. [4]
    Gerhard Gentzen. Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39:176–210, 405–431, 1934.CrossRefMathSciNetGoogle Scholar
  5. [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. [6]
    Jörg Hudelmaier. Bounds for cut elimination in intuitionistic propositional logic. Archive for Mathematical Logic, 31: 331–354, 1992.CrossRefMATHMathSciNetGoogle Scholar
  7. [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.CrossRefGoogle Scholar
  8. [8]
    G.E. Mints. On e-theorems (in russian). Zapiski, 40: 110–118, 1974.MATHGoogle Scholar
  9. [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. [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. [11]
    Dag Prawitz. Natural Deduction, volume 3 of Acta Universitatis Stockholmiensis. Stockholm Studies in Philosophy. Almqvist amp; Wiksell, Stockholm, 1965.Google Scholar
  12. [12]
    Dan Sahlin, Torkel Franzen, and Seif Haridi. An intuitionistic predicate logic theorem prover. Journal of Logic and Computation, 2 (6): 619–656, 1992.CrossRefMATHMathSciNetGoogle Scholar
  13. [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. [14]
    N. Shankar. Proof search in intuitionistic sequent calculus, 1991.Google Scholar
  15. [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. [16]
    Martin Stein. Interpretationen der Heyting-Arithmetik endlicher Typen. PhD thesis, Universität Münster, Fachbereich Mathematik, 1976.Google Scholar
  17. [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. [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. [19]
    Anton Wallner. Komplexe Existenzbeweise in der Arithmetik. Master’s thesis, Mathematisches Institut der Universität München, 1993.Google Scholar
  20. [20]
    Hermann Weyl. Uber die neue Grundlagenkrise der Mathematik. Mathematische Zeitschrift, 10, 1921.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Ulrich Berger
    • 1
  • Helmut Schwichtenberg
    • 1
  1. 1.Mathematisches Institutder Universität MünchenMünchenGermany

Personalised recommendations