Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Computer Science Logic

CSL 1991: Computer Science Logic pp 316–325Cite as

A cut-elimination procedure designed for evaluating proofs as programs

  • Conference paper
  • First Online:

  • 130 Accesses

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

Abstract

This paper describes a method which can be used to determine output values from given input values of programs taking the form of formal proofs. The proofs are constructed in a logic calculus which may include user-defined non-logical inference rules. This calculus is complete in the sense that each computable function can be computed by means of a proof in this calculus. The evaluation method is based mainly on Gentzen's cut-elimination procedure. However the presence of non-logical inference rules requires additional steps to eliminate these rules. Termination of the method is proved by assigning constructive ordinal numbers.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alexi, M., Extraction and verification of programs by analysis of formal proofs, TCS 61 (1988) 225–258

    Google Scholar 

  2. Bachmann, H., Transfinite Zahlen, Springer Verlag, Berlin 1955

    Google Scholar 

  3. Bates, J.L., A logic for correct program development, Cornell Univ. 1979

    Google Scholar 

  4. Bates, J.L. a. Constable, R.L., Definition of Micro-PRL, Tech. Rp. 82-492, Cornell Univ. 1981

    Google Scholar 

  5. Bates, J.L. a. Constable, R.L., Proofs as programs, ACM Trans. on Progr. Lang. a. Syst. 7,1 (1985) 113–136

    Google Scholar 

  6. Bornschein, C., Implementierung eines Verfahrens zur Herleitungstransformation, Diplomarbeit, Technische Universität München 1989

    Google Scholar 

  7. Constable, R.L., Proofs as Programs, Inf. Process. Lett. 16,3 (1983) 105–112

    Google Scholar 

  8. Constable, R.L. a. Bates, J.L., The nearly ultimate PRL, Techn. Rep. 83-551, Cornell Univ. 1983

    Google Scholar 

  9. Gallier, J.H., Logic for Computer Science, New York 1986

    Google Scholar 

  10. Gentzen, G., Untersuchungen über das logische Schließen, Math. Zeitschrift 39 (1935) 176–210, 405–431

    Google Scholar 

  11. Hayashi, S., PX: A System extracting Programs from Proofs

    Google Scholar 

  12. Manna, Z. a. Waldinger, R., A deductive approach to program synthesis, ACM Trans. on Progr. Lang. a. Syst. 2,1 (1980) 92–121

    Google Scholar 

  13. Martin-Löf, P., Constructive mathematics and computer programming, 6th. Intern. Congr. Logic, Method. a. Philos. of Science, Hannover 1979

    Google Scholar 

  14. Regensburger, F., Implementierung eines Schnitteliminationsverfahrens, Diplomarbeit, Technische Universität München 1989

    Google Scholar 

  15. Schütte, K., Proof theory, Springer Verlag, Berlin 1977

    Google Scholar 

  16. Schwichtenberg, H., LCF with realizing terms: a framework for the development and verification of programs, 1988

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fakultät für Informatik, Universität der Bundeswehr München, D-8014, Neubiberg

    Ulf R. Schmerl

Authors
  1. Ulf R. Schmerl
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Egon Börger Gerhard Jäger Hans Kleine Büning Michael M. Richter

Rights and permissions

Reprints and permissions

Copyright information

© 1992 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schmerl, U.R. (1992). A cut-elimination procedure designed for evaluating proofs as programs. In: Börger, E., Jäger, G., Kleine Büning, H., Richter, M.M. (eds) Computer Science Logic. CSL 1991. Lecture Notes in Computer Science, vol 626. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023777

Download citation

  • DOI: https://doi.org/10.1007/BFb0023777

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-47285-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation