20 found
Order:
  1.  56
    Handbook of Constructive Mathematics.Douglas Bridges, Hajime Ishihara, Michael Rathjen & Helmut Schwichtenberg (eds.) - 2023 - Cambridge: Cambridge University Press.
    Constructive mathematics – mathematics in which ‘there exists’ always means ‘we can construct’ – is enjoying a renaissance. Fifty years on from Bishop’s groundbreaking account of constructive analysis, constructive mathematics has spread out to touch almost all areas of mathematics and to have profound influence in theoretical computer science. This handbook gives the most complete overview of modern constructive mathematics, with contributions from leading specialists surveying the subject’s myriad aspects. Major themes include: constructive algebra and geometry, constructive analysis, constructive topology, (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  2.  50
    Eine Klassifikation der ε 0 ‐Rekursiven Funktionen.Helmut Schwichtenberg - 1971 - Mathematical Logic Quarterly 17 (1):61-74.
    No categories
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  3.  38
    Refined program extraction from classical proofs.Ulrich Berger, Wilfried Buchholz & Helmut Schwichtenberg - 2002 - Annals of Pure and Applied Logic 114 (1-3):3-25.
    The paper presents a refined method of extracting reasonable and sometimes unexpected programs from classical proofs of formulas of the form ∀x∃yB . We also generalize previously known results, since B no longer needs to be quantifier-free, but only has to belong to a strictly larger class of so-called “goal formulas”. Furthermore we allow unproven lemmas D in the proof of ∀x∃yB , where D is a so-called “definite” formula.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  4.  42
    Embedding classical in minimal implicational logic.Hajime Ishihara & Helmut Schwichtenberg - 2016 - Mathematical Logic Quarterly 62 (1-2):94-101.
    Consider the problem which set V of propositional variables suffices for whenever, where, and ⊢c and ⊢i denote derivability in classical and intuitionistic implicational logic, respectively. We give a direct proof that stability for the final propositional variable of the (implicational) formula A is sufficient; as a corollary one obtains Glivenko's theorem. Conversely, using Glivenko's theorem one can give an alternative proof of our result. As an alternative to stability we then consider the Peirce formula. It is an easy consequence (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  5. Minimal from classical proofs.Helmut Schwichtenberg & Christoph Senjak - 2013 - Annals of Pure and Applied Logic 164 (6):740-748.
    Let A be a formula without implications, and Γ consist of formulas containing disjunction and falsity only negatively and implication only positively. Orevkov and Nadathur proved that classical derivability of A from Γ implies intuitionistic derivability, by a transformation of derivations in sequent calculi. We give a new proof of this result , where the input data are natural deduction proofs in long normal form involving stability axioms for relations; the proof gives a quadratic algorithm to remove the stability axioms. (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  6.  67
    On bar recursion of types 0 and 1.Helmut Schwichtenberg - 1979 - Journal of Symbolic Logic 44 (3):325-329.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  7.  61
    An upper bound for reduction sequences in the typed λ-calculus.Helmut Schwichtenberg - 1991 - Archive for Mathematical Logic 30 (5-6):405-408.
  8.  85
    Program Extraction from Normalization Proofs.Ulrich Berger, Stefan Berghofer, Pierre Letouzey & Helmut Schwichtenberg - 2006 - Studia Logica 82 (1):25-49.
    This paper describes formalizations of Tait's normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs programs are machine-extracted that implement variants of the well-known normalization-by-evaluation algorithm. The case study is used to test and compare the program extraction machineries of the three proof assistants in a non-trivial setting.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  9.  33
    Logic for Gray-code Computation.Hideki Tsuiki, Helmut Schwichtenberg, Kenji Miyamoto & Ulrich Berger - 2016 - In Peter Schuster & Dieter Probst (eds.), Concepts of Proof in Mathematics, Philosophy, and Computer Science. Boston: De Gruyter. pp. 69-110.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  43
    Dialectica interpretation of well-founded induction.Helmut Schwichtenberg - 2008 - Mathematical Logic Quarterly 54 (3):229-239.
    From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well-founded recursion can be used to Dialectica interpret well-founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  22
    (2 other versions)Characterising polytime through higher type recursion.Stephen J. Bellantoni, Karl-Heinz Niggl & Helmut Schwichtenberg - 2000 - Annals of Pure and Applied Logic 104 (1-3):17-30.
  12.  52
    (1 other version)Finite notations for infinite terms.Helmut Schwichtenberg - 1998 - Annals of Pure and Applied Logic 94 (1-3):201-222.
    Buchholz presented a method to build notation systems for infinite sequent-style derivations, analogous to well-known systems of notation for ordinals. The essential feature is that from a notation one can read off by a primitive recursive function its n th predecessor and, e.g. the last rule applied. Here we extend the method to the more general setting of infinite terms, in order to make it applicable in other proof-theoretic contexts as well as in recursion theory. As examples, we use the (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  13.  49
    Montréal, Québec, Canada May 17–21, 2006.Jeremy Avigad, Sy Friedman, Akihiro Kanamori, Elisabeth Bouscaren, Philip Kremer, Claude Laflamme, Antonio Montalbán, Justin Moore & Helmut Schwichtenberg - 2007 - Bulletin of Symbolic Logic 13 (1).
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14.  21
    (1 other version)Proof and Computation.Klaus Mainzer, Peter Schuster & Helmut Schwichtenberg (eds.) - 1995 - World Scientific.
    Proceedings of the NATO Advanced Study Institute on Proof and Computation, held in Marktoberdorf, Germany, July 20 - August 1, 1993.
    Direct download  
     
    Export citation  
     
    Bookmark  
  15.  44
    Tutorial for Minlog.Laura Crosilla, Monika Seisenberger & Helmut Schwichtenberg - 2011 - Minlog Proof Assistant - Freely Distributed.
    This is a tutorial for the Minlog Proof Assistant, version 5.0.
    Direct download  
     
    Export citation  
     
    Bookmark  
  16.  86
    Monotone majorizable functionals.Helmut Schwichtenberg - 1999 - Studia Logica 62 (2):283-289.
    Several properties of monotone functionals (MF) and monotone majorizable functionals (MMF) used in the earlier work by the author and van de Pol are proved. It turns out that the terms of the simply typed lambda-calculus define MF, but adding primitive recursion, and even monotonic primitive recursion changes the situation: already Z.Z(1 — sg) is not MMF. It is proved that extensionality is not Dialectica-realizable by MMF, and a simple example of a MF which is not hereditarily majorizable is given.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  17.  24
    (1 other version)A Short Introduction to Intuitionistic Logic.Helmut Schwichtenberg - 2002 - Bulletin of Symbolic Logic 8 (4):520-521.
  18.  48
    Charles Parsons. On a number theoretic choice schema and its relation to induction. Intuitionism and proof theory, Proceedings of the summer conference at Buffalo N.Y. 1968, edited by A. Kino, J. Myhill, and R. E. Vesley, Studies in logic and the foundations of mathematics, North-Holland Publishing Company, Amsterdam and London 1970, pp. 459–473. - Charles Parsons. Review of the foregoing. Zentralblatt für Mathematik and ihre Grenzgebiete, vol. 202 , pp. 12–13. - Charles Parsons. On n-quantifier induction. The journal of symbolic logic, vol. 37 , pp. 466–482. [REVIEW]Helmut Schwichtenberg - 1974 - Journal of Symbolic Logic 39 (2):342.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  19.  37
    (1 other version)Logic from computer science, Proceedings of a workshop held November 13–17, 1989, edited by Y. N. Moschovakis, Mathematical Sciences Research Institute publications, vol. 21, Springer-Verlag, New York etc. 1992, xi + 608 pp. [REVIEW]Helmut Schwichtenberg - 1995 - Journal of Symbolic Logic 60 (3):1021-1022.
  20.  32
    Review: Charles Parsons, A. Kino, J. Myhill, R. E. Vesley, On a Number Theoretic Choice Schema and its Relation to Induction; Charles Parsons, Review of the Foregoing; Charles Parsons, On $n$-Quantifier Induction. [REVIEW]Helmut Schwichtenberg - 1974 - Journal of Symbolic Logic 39 (2):342-342.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark