A constructive valuation interpretation for classical logic and its use in witness extraction

  • Franco Barbanera
  • Stefano Berardi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)


A constructive interpretation of classical arithmetic in terms of a Kripke-like valuation semantics of proofs is presented. We use this interpretation for motivating a constructive procedure, based on reduction rules, for extracting witnesses from proofs of ∑ 1 0 sentences in classical arithmetic.


Classical Logic Intuitionistic Logic Reduction Rule Double Negation Peano Arithmetic 
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. [BB]
    Barbanera F., Berardi S. Witness extraction in classical logic through normalization, Technical Report Dipartimento di Informatica Universita' di Torino, 1991.Google Scholar
  2. [Ber]
    Berardi S. A semantic purely intuitionistic proof of Takeuti's conjecture. Rendiconti del Seminario Matematico Univers. Politecn. Torino, vol.46, 59–89, 1988.Google Scholar
  3. [FFKD]
    Felleisen M., Friedman D., Kohlbeker E., Duba B. Reasoning with continuations. In Proceedings of the First Annual Symposium on Logic in Computer Science, 131–141, 1986.Google Scholar
  4. [Fried]
    Friedman H. Classically and intuitionistically provable recursive functions. In Scott D.S. and Muller G.H. editors, Higher Set Theory, vol.699 of Lecture Notes in Mathematics, 21–28, Springer Verlag, 1978.Google Scholar
  5. [GN]
    Geuvers H., Nederhof M.J. A simple modular proof of the strong normalization for the Calculus of Construction. To appear in Journal of functional Programming.Google Scholar
  6. [Gir]
    Girard J.-Y. Une extension de l'interpretation de Gödel a l'analyse, et son application a l'elimination des coupures dans l'analyse et la theorie des types. In Proceedings of the second Scandivian Logic Symposium, eds. J.E. Fenstad, Amsterdam, North-Holland, 63–92, 1971.Google Scholar
  7. [Griff]
    Griffin T.G. A formulae as types notion of control. In Conference Record of the Seventeenth Annual ACM Symposium on Principle of Programming Languages, 1990.Google Scholar
  8. [HHP]
    Harper R., Honsell F., Plotkin G. A framework for defining logics. Proceedings of the symposium on Logic in Computer Science. Ithaca, New York, IEEE, Washington D.C. 1987.Google Scholar
  9. [Kre]
    Kreisel G. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 23:155–182, 1958.Google Scholar
  10. [Plot]
    Plotkin G. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 125–159, 1975.Google Scholar
  11. [Pra 1]
    Prawitz D. Natural deduction, a proof theoretical study. Stockolm, Almqvist and Winskell, 1965.Google Scholar
  12. [Pra 2]
    Prawitz D. Validity and normalizability of proofs in 1-st and 2-nd order classical and intuitionistic logic. In Atti del I Congresso Italiano di Logica, Napoli, Bibliopolis, 11–36, 1981.Google Scholar
  13. [Schü]
    Schütte K. Proof Theory. Springer Verlag, 1977.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Franco Barbanera
    • 1
  • Stefano Berardi
    • 1
  1. 1.Dipartimento di InformaticaTorinoItaly

Personalised recommendations