34 found
Order:
Disambiguations
Helmut Schwichtenberg [30]H. Schwichtenberg [13]
  1.  4
    Basic Proof Theory.A. S. Troelstra & H. Schwichtenberg - 2001 - Bulletin of Symbolic Logic 7 (2):280-280.
    Direct download  
     
    Export citation  
     
    Bookmark   71 citations  
  2.  45
    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   3 citations  
  3.  9
    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 (6 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  4.  56
    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 (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  5.  14
    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  
  6.  39
    An Upper Bound for Reduction Sequences in the Typed Λ-Calculus.Helmut Schwichtenberg - 1991 - Archive for Mathematical Logic 30 (5-6):405-408.
  7.  24
    Eine Klassifikation der ɛ0-Rekursiven Funktionen.Helmut Schwichtenberg - 1971 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 17 (1):61-74.
    No categories
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   9 citations  
  8.  10
    Proofs and Computations.Helmut Schwichtenberg - 2012 - Cambridge University Press.
    Driven by the question, 'What is the computational content of a (formal) proof?', this book studies fundamental interactions between proof theory and computability. It provides a unique self-contained text for advanced students and researchers in mathematical logic and computer science. Part I covers basic proof theory, computability and Gödel's theorems. Part II studies and classifies provable recursion in classical systems, from fragments of Peano arithmetic up to Π11-CA0. Ordinal analysis and the (Schwichtenberg-Wainer) subrecursive hierarchies play a central role and are (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  24
    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   6 citations  
  10.  21
    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 (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  15
    Eine Klassifikation der ε0‐Rekursiven Funktionen.Helmut Schwichtenberg - 1971 - Mathematical Logic Quarterly 17 (1):61-74.
    Direct download (4 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   9 citations  
  12.  12
    Higher Type Recursion, Ramification and Polynomial Time.Stephen J. Bellantoni, Karl-Heinz Niggl & Helmut Schwichtenberg - 2000 - Annals of Pure and Applied Logic 104 (1-3):17-30.
    It is shown how to restrict recursion on notation in all finite types so as to characterize the polynomial-time computable functions. The restrictions are obtained by using a ramified type structure, and by adding linear concepts to the lambda calculus.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  13.  5
    Grigori Mints. A Short Introduction to Intuitionistic Logic. The University Series in Mathematics. Kluwer Academic/Plenum Publishers, New York Etc. 2000, Ix + 131 Pp. [REVIEW]Helmut Schwichtenberg - 2002 - Bulletin of Symbolic Logic 8 (4):520-521.
  14. 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.
  15.  16
    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   1 citation  
  16.  15
    Bemerkungen zum Spektralproblem.D. Rödding & H. Schwichtenberg - 1972 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 18 (1-3):1-12.
    No categories
    Direct download (2 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  17.  52
    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 (8 more)  
     
    Export citation  
     
    Bookmark  
  18.  12
    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.
  19.  12
    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)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  20. Bemerkungen zum Spektralproblem.D. Rödding & H. Schwichtenberg - 1972 - Mathematical Logic Quarterly 18 (1‐3):1-12.
    Direct download (5 more)  
    Translate
     
     
    Export citation  
     
    Bookmark   1 citation  
  21.  7
    Embedding Classical in Minimal Implicational Logic.Hajime Ishihara & Helmut Schwichtenberg - 2016 - Mathematical Logic Quarterly 62 (1-2):94-101.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  22.  6
    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. De Gruyter. pp. 69-110.
    Direct download  
     
    Export citation  
     
    Bookmark  
  23.  6
    Rose H. E.. Subrecursion. Functions and Hierarchies. Oxford Logic Guides, No. 9. Clarendon Press, Oxford University Press, Oxford and New York 1984, Xiii + 191 Pp. [REVIEW]H. Schwichtenberg - 1987 - Journal of Symbolic Logic 52 (2):563-565.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  24.  9
    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  
  25.  5
    Review: Y. N. Moschovakis, Logic From Computer Science, Proceedings of a Workshop Held November 13-17 1989; , Logics for Negation as Failure. [REVIEW]Helmut Schwichtenberg - 1995 - Journal of Symbolic Logic 60 (3):1021-1022.
  26.  7
    Review: H. E. Rose, Subrecursion. Functions and Hierarchies. [REVIEW]H. Schwichtenberg - 1987 - Journal of Symbolic Logic 52 (2):563-565.
  27.  4
    Cohors-Fresenborg E.. Mathematik mit Kalkülen and Maschinen. Mit Vorwort von Dieter Rödding. Logik und Grundlagen der Mathematik, Bd. 20. Vieweg, Braunschweig 1977, VIII + 184 S. [REVIEW]H. Schwichtenberg - 1980 - Journal of Symbolic Logic 45 (2):380-381.
    Direct download (3 more)  
    Translate
     
     
    Export citation  
     
    Bookmark  
  28. Review: E. Cohors-Fresenborg, Dieter Rodding, Mathematik mit Kalkulen und Maschinen. [REVIEW]H. Schwichtenberg - 1980 - Journal of Symbolic Logic 45 (2):380-381.
    Translate
     
     
    Export citation  
     
    Bookmark  
  29. La Sorbonne, Paris, France, July 23–31, 2000.C. Parsons Kanamori, A. Razborov, H. Schwichtenberg, J. Steel, S. Todorcevic, A. Wilkie, R. Cori, M. Dickmann, J. Dubucs & J. B. Joinet - 2001 - Bulletin of Symbolic Logic 7 (1).
  30. REVIEWS-Refined Program Extraction From Classical Proofs.U. Berger, W. Buchholz, H. Schwichtenberg & N. Danner - 2003 - Bulletin of Symbolic Logic 9 (1):47-48.
     
    Export citation  
     
    Bookmark  
  31. Proof and Computation.Klaus Mainzer, Peter Schuster & Helmut Schwichtenberg (eds.) - 2018 - World Scientific.
    No categories
     
    Export citation  
     
    Bookmark  
  32. 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  
  33. The 1996-97 ASL Winter Meeting Will Be Held in Conjunction with the Annual Meeting of the American Mathematical Society During January 8-11, 1997, in San Diego, California. The 1996-97 ASL Annual Meeting Will Be Held March 22-25, 1997, at the Massachusetts Institute of Technology in Cambridge, Massachusetts. Chair of the Local Organizing Com-Mittee is Sy Friedman. [REVIEW]A. Louveau, Y. Moschovakis, L. Pacholski, H. Schwichtenberg, T. Slaman, J. Truss, H. D. Macpherson, A. Slomson & S. Wainer - 1996 - Bulletin of Symbolic Logic 2:121.
  34. REVIEWS-Basic Proof Theory.A. Troelstra, H. Schwichtenberg & Roy Dyckhoff - 2001 - Bulletin of Symbolic Logic 7 (2):280.