Proofs Verifying Programs and Programs Producing Proofs: A Conceptual Analysis

  • Dag Prawitz


I shall deal here with conceptual questions concerning two related phenomena: 1) the use of deductive machinery to verify the correctness of computer programs, and 2) the running of programs on computers to produce proofs.


Inference Rule Type Theory Formal Proof Natural Deduction Combinatory Logic 
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.
    A. Church: Introduction to Mathematical Logic (Princeton University Press, Princeton 1956)Google Scholar
  2. 2.
    H. Curry, R. Feys: Combinatory Logic, vol. 1 (North Holland, Amsterdam 1958)Google Scholar
  3. 3.
    M. Detlefsen, M. Luker: The four-color theorem and mathematical proof. The Journal of Philosophy 77 (1980) pp 803–820CrossRefGoogle Scholar
  4. 4.
    G. Gentzen: Untersuchungen ber das logische Schliessen. Mathematische Zeitschrift 39 (1935) pp 176–210, 405-431CrossRefGoogle Scholar
  5. 5.
    A. Heyting: Intuitionism, An Introduction (North Holland, Amsterdam 1956)Google Scholar
  6. 6.
    W. A. Howard: The formulae-as-types notion of constructions. In: To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, ed by J. P. Seldin and J. R. Hindley (Academic Press 1980) pp 479–490Google Scholar
  7. 7.
    A. N. Kolmogorov: Zur Deutung der intuitionistischen Logik. Mathematische Zeitschrift 35 (1932) pp 58–65CrossRefGoogle Scholar
  8. 8.
    P. Martin-Löf: An intuitionistic theory of types: Predicative part. In: Logic Colloquium’ 73, ed by H. E. Rose and J. C. Shepherdson (North Holland, Amsterdam 1975) pp 73–118Google Scholar
  9. 9.
    P. Martin-Löf: Constructive mathematics and computer programming. In: Logic, Methodology and Philosophy of Science IV, ed by L. J. Cohen et al. (North-Holland, Amsterdam 1982) pp 153–175Google Scholar
  10. 10.
    P. Martin-Löf: Intuitionistic Type Theory (Bibliopolis, Napoli 1984)Google Scholar
  11. 11.
    P. Martin-Löf: On the meanings of the logical constants and the justifications of the logical laws. In: Atti degli Incontri di Logica Matematica 2 Dipartimento di Matematica, Universit di Siena (1985) pp 203–281. Reprinted in Nordic Journal of Philosophical Logic 1 (1996) pp 11-60Google Scholar
  12. 12.
    D. Prawitz: Natural Deduction. A Proof-Theoretical Study (Almqvist and Wiksell, Stockholm 1965). Reprinted (Dover Publications, New York 2006)Google Scholar
  13. 13.
    D. Prawitz: Ideas and results in proof theory. In: Proceedings of the Second Scandinavian Logic Symposium, ed by J. Fenstad (North-Holland, Amsterdam, 1971) pp 237–309Google Scholar
  14. 14.
    D. Prawitz: Validity of inference. In: Proceedings from the 2nd Launer Symposium on the Occasion of the Presentation of the Launer Prize at Bern 2006 (2009) To appearGoogle Scholar
  15. 15.
    D. Prawitz, H. Prawitz and N. Voghera: A mechanical proof procedure and its realization in an electronic computer. Journal of the Association for Computing Machinery 7 (1960) pp 102–128Google Scholar
  16. 16.
    P. Teller: Computer proof. The Journal of Philosophy 77 (1980) pp 797–803CrossRefGoogle Scholar
  17. 17.
    T. Tymoczko: The four-color problem and its philosophical significance. The Journal of Philosophy 76 (1979) pp 57–83CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Italia 2008

Authors and Affiliations

  • Dag Prawitz
    • 1
  1. 1.Stockholms UniversitetFilosofiska institutionenStockholmSweden

Personalised recommendations