{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T10:40:24Z","timestamp":1699958424947},"reference-count":10,"publisher":"Wiley","issue":"3","license":[{"start":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T00:00:00Z","timestamp":1210032000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2008,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>From a classical proof that the gcd of natural numbers <jats:italic>a<\/jats:italic><jats:sub>1<\/jats:sub> and <jats:italic>a<\/jats:italic><jats:sub>2<\/jats:sub> is a linear combination of the two, we extract by G\u00f6del's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well\u2010founded recursion can be used to Dialectica interpret well\u2010founded 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 algorithm close to Euclid's. (\u00a9 2008 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200710045","type":"journal-article","created":{"date-parts":[[2008,5,6]],"date-time":"2008-05-06T07:52:19Z","timestamp":1210060339000},"page":"229-239","source":"Crossref","is-referenced-by-count":6,"title":["Dialectica interpretation of well\u2010founded induction"],"prefix":"10.1002","volume":"54","author":[{"given":"Helmut","family":"Schwichtenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2008,5,6]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(01)00073-2"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00014-2"},{"key":"e_1_2_1_4_2","doi-asserted-by":"crossref","unstructured":"U.Berger andH.Schwichtenberg The greatest common divisor: a case study for program extraction from classical proofs. In: Types for Proofs and Programs. International Workshop TYPES '95 Torino Italy June 1995. Selected Papers (S. Berardi and M. Coppo eds.). Lecture Notes in Computer Science 1158 pp. 36\u201346 (Springer\u2010Verlag 1996).","DOI":"10.1007\/3-540-61780-9_60"},{"key":"e_1_2_1_5_2","unstructured":"A.Dragalin New kinds of realizability. In: Abstracts of the 6th International Congress of Logic Methodology and Philosophy of Sciences pp. 20\u201324 Hannover Germany 1979."},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"H.Friedman Classically and intuitionistically provably recursive functions. In: Higher Set Theory (D. Scott and G. M\u00fcller eds.). Lecture Notes in Mathematics 669 pp. 21\u201328 (Springer\u2010Verlag 1978).","DOI":"10.1007\/BFb0103100"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"e_1_2_1_8_2","unstructured":"M.\u2010D.Hernest Feasible programs from (non\u2010constructive) proofs by the light (monotone) Dialectica interpretation. Ph. D. thesis Ecole Polytechnique Paris and LMU M\u00fcnchen 2006."},{"key":"e_1_2_1_9_2","unstructured":"K. F.J\u00f8rgensen Finite type arithmetic. Master's thesis University of Roskilde 2001."},{"key":"e_1_2_1_10_2","doi-asserted-by":"crossref","unstructured":"H.Schwichtenberg andS. S.Wainer Ordinal bounds for programs. In: Feasible Mathematics II (P. Clote and J. Remmel eds.) pp. 387\u2013406 (Birkh\u00e4user 1995).","DOI":"10.1007\/978-1-4612-2566-9_13"},{"key":"e_1_2_1_11_2","doi-asserted-by":"crossref","unstructured":"A. S.Troelstra (ed.) Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344 (Springer\u2010Verlag 1973).","DOI":"10.1007\/BFb0066739"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200710045","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200710045","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,14]],"date-time":"2023-11-14T10:25:45Z","timestamp":1699957545000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200710045"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,5,6]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2008,6]]}},"alternative-id":["10.1002\/malq.200710045"],"URL":"https:\/\/doi.org\/10.1002\/malq.200710045","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,5,6]]}}}