{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T22:10:30Z","timestamp":1687558230254},"reference-count":79,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2012,6,26]],"date-time":"2012-06-26T00:00:00Z","timestamp":1340668800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Log. Univers."],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s11787-012-0056-7","type":"journal-article","created":{"date-parts":[[2012,6,25]],"date-time":"2012-06-25T13:58:10Z","timestamp":1340632690000},"page":"485-520","source":"Crossref","is-referenced-by-count":2,"title":["HERBRAND\u2019s Fundamental Theorem in the Eyes of JEAN VAN HEIJENOORT"],"prefix":"10.1007","volume":"6","author":[{"given":"Claus-Peter","family":"Wirth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,6,26]]},"reference":[{"key":"56_CR1","first-page":"63","volume":"4","author":"F. Abeles","year":"1994","unstructured":"Abeles F.: Herbrand\u2019s Fundamental Theorem and the beginning of logic programming. Modern Logic 4, 63\u201373 (1994)","journal-title":"Modern Logic"},{"key":"56_CR2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1023\/B:JARS.0000009552.54063.f3","volume":"31","author":"P.B. Andrews","year":"2003","unstructured":"Andrews P.B.: Herbrand Award acceptance speech. J. Autom. Reason. 31, 169\u2013187 (2003)","journal-title":"J. Autom. Reason."},{"key":"56_CR3","doi-asserted-by":"crossref","unstructured":"Anellis, I.H.: The L\u00f6wenheim\u2013Skolem Theorem, theories of quantification, and proof theory. In: Drucker, T. (ed.) Perspectives on the History of Mathematical Logic, pp. 71\u201383. Birkh\u00e4user\/Springer, Berlin (1991)","DOI":"10.1007\/978-0-8176-4769-8_6"},{"key":"56_CR4","unstructured":"Anellis, I.H.: Logic and its history in the work and writings of Jean van Heijenoort. Modern Logic Publ., Ames (1992)"},{"key":"56_CR5","unstructured":"Autexier, S.: Hierarchical contextual reasoning. Ph.D. thesis, FR Informatik, Saarland University (2003)"},{"key":"56_CR6","doi-asserted-by":"crossref","unstructured":"Autexier, S.: The core calculus. In: Nieuwenhuis, R. (ed.) 20th Int. Conf. on Automated Deduction, Tallinn, 2005. Lecture Notes in Artificial Intelligence, no. 3632, pp. 84\u201398. Springer, Berlin (2005)","DOI":"10.1007\/11532231_7"},{"key":"56_CR7","unstructured":"Autexier, S.: Benzm\u00fcller, C., Dietrich, D., Meier, A., Wirth, C.-P.: A generic modular data structure for proof attempts alternating on ideas and granularity. In: Kohlhase, M. (ed.) 4th Int. Conf. on Mathematical Knowledge Management (MKM), Bremen, 2005 (revised selected papers). Lecture Notes in Artificial Intelligence, no. 3863, pp. 126\u2013142. Springer, Berlin (2006). http:\/\/www.ags.uni-sb.de\/~cp\/p\/pds"},{"key":"56_CR8","doi-asserted-by":"crossref","unstructured":"Baaz, M., Ferm\u00fcller, C.G.: Non-elementary speedups between different versions of tableaux. In: Baumgartner, P., H\u00e4hnle, R., Posegga, J. (eds.) 5th Int. Conf. on Tableaus and Related Methods, St. Goar (Germany). Lecture Notes in Artificial Intelligence, no. 918, pp. 217\u2013230. Springer, Berlin (1995)","DOI":"10.1007\/3-540-59338-1_38"},{"key":"56_CR9","doi-asserted-by":"crossref","unstructured":"Baaz, M., Leitsch, A.: Methods of functional extension. Collegium Logicum\u2014Annals of the Kurt G\u00f6del Society 1, 87\u2013122 (1995)","DOI":"10.1007\/978-3-7091-9394-5_7"},{"key":"56_CR10","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: The even more liberalized \u03b4-rule in free-variable semantic tableaus. In: Gottlob, G., Leitsch, A., Mundici, D. (eds.) Computational Logic and Proof Theory. Proc. 3rd Kurt G\u00f6del Colloquium. Lecture Notes in Computer Science, no. 713, pp. 108\u2013119. Springer, Berlin (1993)","DOI":"10.1007\/BFb0022559"},{"key":"56_CR11","doi-asserted-by":"crossref","unstructured":"Berka, K., Kreiser, L. (eds.): Logik-Texte\u2014Kommentierte Auswahl zur Geschichte der modernen Logik, 2nd rev. edn. (1st edn. 1971; 4th rev. edn. 1986.) Akademie-Verlag, Berlin (1973)","DOI":"10.1515\/9783112611302"},{"key":"56_CR12","unstructured":"Bernays, P.: \u00dcber den Zusammenhang des Herbrand schen Satzes mit den neueren Ergebnissen von Sch\u00fctte und Stenius. Proceedings of the International Congress of Mathematicians 1954 (Groningen and Amsterdam). Noordhoff and North-Holland\/Elsevier (1957)"},{"key":"56_CR13","unstructured":"Brady, G.: From Peirce to Skolem: A Neglected Chapter in the History of Logic. North-Holland\/Elsevier (2000)"},{"key":"56_CR14","doi-asserted-by":"crossref","unstructured":"Cohen, R.S., Wartofsky, M.W. (eds.): Proc. of the Boston Colloquium for the Philosophy of Science, 1964\u20131966: In: Memory of norwood russell hanson, Boston Studies in the Philosophy of Science, no. 3. D. Reidel, Dordrecht (1967)","DOI":"10.1007\/978-94-010-3508-8"},{"key":"56_CR15","unstructured":"Dietrich, D.: Proof planning with compiled strategies. PhD thesis, FR Informatik, Saarland University (2011)"},{"key":"56_CR16","doi-asserted-by":"crossref","first-page":"699","DOI":"10.1090\/S0002-9904-1963-10990-8","volume":"69","author":"B. Dreben","year":"1963","unstructured":"Dreben B., Andrews P.B., Aanderaa S.: False lemmas in Herbrand. Bull. Am. Math. Soc. 69, 699\u2013706 (1963)","journal-title":"Bull. Am. Math. Soc."},{"issue":"3","key":"56_CR17","doi-asserted-by":"crossref","first-page":"393","DOI":"10.2307\/2270454","volume":"31","author":"B. Dreben","year":"1963","unstructured":"Dreben B., Denton J.: A supplement to Herbrand. J. Symbolic Logic 31(3), 393\u2013398 (1963)","journal-title":"J. Symbolic Logic"},{"key":"56_CR18","volume-title":"Politics, Logic and Love\u2014The Life of Jean van Heijenoort","author":"A.B. Feferman","year":"1993","unstructured":"Feferman A.B.: Politics, Logic and Love\u2014The Life of Jean van Heijenoort. A K Peters, Wellesley (1993)"},{"key":"56_CR19","unstructured":"Feferman, S.: Jean van Heijenoort\u2019s scholarly work. In: [18, pp. 371\u2013390] (1993)"},{"key":"56_CR20","doi-asserted-by":"crossref","unstructured":"Fitting, M.: First-Order Logic and Automated Theorem Proving, 2nd rev. edn. (1st edn. 1990). Springer, Berlin (1996)","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"56_CR21","unstructured":"Frege, G.: Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von L. Nebert, Halle an der Saale, 1879. Corrected facsimile in [22]. Reprint of pp. III\u2013VIII and pp. 1\u201354 in [11, pp. 48\u2013106]. English translation in [32, pp. 1\u201382]"},{"key":"56_CR22","unstructured":"Frege, G.: Begriffsschrift und andere Aufs\u00e4tze. Wissenschaftliche Buchgesellschaft, Darmstadt, 1964, Zweite Auflage, mit Edmund Husserls und Heinrich Scholz\u2019 Anmerkungen, herausgegeben von Ignacio Angelelli"},{"key":"56_CR23","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Woods, J. (eds.): Handbook of the History of Logic. North-Holland\/ Elsevier (2004)","DOI":"10.1007\/978-94-017-0466-3"},{"key":"56_CR24","unstructured":"Gentzen, G.: Untersuchungen \u00fcber das logische Schlie\u00dfen. Math. Z. 39, 176\u2013210, 405\u2013431 (1935). Also in [11, pp. 192\u2013253]. English translation in [25]"},{"key":"56_CR25","unstructured":"Gentzen, G.: In: Szabo, M.E. (ed.) The Collected Papers of Gerhard Gentzen. North-Holland\/Elsevier (1969)"},{"key":"56_CR26","doi-asserted-by":"crossref","unstructured":"G\u00f6del, K.: Die Vollst\u00e4ndigkeit der Axiome des logischen Funktionenkalk\u00fcls. Monatshefte f\u00fcr Mathematik und Physik 37, 349\u2013360 (1930). With English translation also in [27, vol. I, pp. 102\u2013123]","DOI":"10.1007\/BF01696781"},{"key":"56_CR27","unstructured":"G\u00f6del, K.: Collected Works. Oxford University Press, 1986ff. Eds. Feferman, S., Dawson, J.W. Jr., Goldfarb, W., Heijenoort, J.v., Kleene, S.C., Parsons, C., Sieg, W., et\u00a0al."},{"key":"56_CR28","first-page":"103","volume":"3","author":"W. Goldfarb","year":"1993","unstructured":"Goldfarb W.: Herbrand\u2019s error and G\u00f6del\u2019s correction. Modern Logic 3, 103\u2013118 (1993)","journal-title":"Modern Logic"},{"key":"56_CR29","first-page":"1382","volume":"55","author":"G. Gonthier","year":"2008","unstructured":"Gonthier G.: Formal proof\u2014the Four-Color Theorem. Notices Am. Math. Soc. 55, 1382\u20131393 (2008)","journal-title":"Notices Am. Math. Soc."},{"key":"56_CR30","doi-asserted-by":"crossref","unstructured":"Heijenoort, J.v.: Logic as a calculus and logic as a language. Synthese 17, 324\u2013330 (1967). Also in [14, pp. 440\u2013446]. Also in [38, pp. 11\u201316]","DOI":"10.1007\/BF00485036"},{"key":"56_CR31","unstructured":"Heijenoort, J.v.: On the relation between the falsifiability tree method and the Herbrand method in quantification theory. Unpublished typescript, Nov 20, 1968, 12\u00a0pp.; Jean van Heijenoort Papers, 1946\u20131988. Archives of American Mathematics, Center for American History, University of Texas at Austin, Box 3.8\/86\u201333\/1. Copy in Anellis Archives (1968)"},{"key":"56_CR32","unstructured":"Heijenoort, J.v.: From Frege to G\u00f6del: A Source Book in Mathematical Logic, 1879\u20131931, 2nd rev. edn. (1st edn. 1967). Harvard University Press (1971)"},{"key":"56_CR33","unstructured":"Heijenoort, J.v.: Herbrand, Unpublished typescript, May 18, 1975, 15\u00a0pp.; Jean van Heijenoort Papers, 1946\u20131988. Archives of American Mathematics, Center for American History, University of Texas at Austin, Box 3.8\/86-33\/1. Copy in Anellis Archives (1975)"},{"key":"56_CR34","unstructured":"Heijenoort, J.v.: El desarrollo de la teoria de la cuantifcaci\u00f3n. Instituto de Investigaciones Filos\u00f3ficas, Universidad Nacional Aut\u00f3noma de M\u00e9xico (1976)"},{"key":"56_CR35","doi-asserted-by":"crossref","unstructured":"Heijenoort, J.v.: L\u2019\u0153uvre logique de Herbrand et son contexte historique (1982). In: [65, pp. 57\u201385]. Rev. English translation is [37]","DOI":"10.1016\/S0049-237X(08)71877-9"},{"key":"56_CR36","unstructured":"Heijenoort, J.v.: Friedrich Engels and mathematics. In: [38, pp. 123\u2013151]. Previously unpublished manuscript written in 1948 (1986)"},{"key":"56_CR37","unstructured":"Heijenoort, J.v.: Herbrand\u2019s work in logic and its historical context. In: [38, pp. 99\u2013121]. Rev. English translation of [35] (1986)"},{"key":"56_CR38","unstructured":"Heijenoort, J.v.: Selected Essays. Bibliopolis, Napoli, copyright 1985. Also published by Librairie Philosophique J. Vrin, Paris (1986)"},{"key":"56_CR39","unstructured":"Heijenoort, J.v.: Historical development of modern logic. Modern Logic 2, 242\u2013255 (1992). Written in 1974"},{"key":"56_CR40","unstructured":"Herbrand, J.: Recherches sur la th\u00e9orie de la d\u00e9monstration. Ph.D. thesis, Universit\u00e9 de Paris (1930). Th\u00e8ses pr\u00e9sent\u00e9es \u00e0 la facult\u00e9 des Sciences de Paris pour obtenir le grade de docteur \u00e8s sciences math\u00e9matiques\u20141re th\u00e8se: Recherches sur la th\u00e9orie de la d\u00e9monstration\u20142me th\u00e8se: Propositions donn\u00e9es par la facult\u00e9, Les \u00e9quations de Fredholm\u2014Soutenues le 1930 devant la commission d\u2019examen\u2014Pr\u00e9sident: M. Vessiot, Examinateurs: MM. Denjoy, Frechet\u2014Vu et approuv\u00e9, Paris, le 20 Juin 1929, Le doyen de la facult\u00e9 des Sciences, C. Maurain\u2014Vu et permis d\u2019imprimer, Paris, le 20 Juin 1929, Le recteur de l\u2019Academie de Paris, S. Charlety\u2014No. d\u2019ordre 2121, S\u00e9rie A, No. de S\u00e9rie 1252\u2014Imprimerie J. Dziewulski, Varsovie\u2014Univ. de Paris. Also in Prace Towarzystwa Naukowego Warszawskiego, Wydzia\u0142 III Nauk Matematyczno-Fizychnych, Nr. 33, Warszawa. Also in [42, pp. 35\u2013153]. Annotated English translation \u201cInvestigations in Proof Theory\u201d by Warren Goldfarb (Chapters 1\u20134) and Burton Dreben and Jean van Heijenoort (Chapter 5) with a brief introduction by Goldfarb and extended notes by Goldfarb (Notes A\u2013C, K\u2013M, O), Dreben (Notes F\u2013I), Dreben and Goldfarb (Notes D, J, and N), and Dreben, George Huff, and Theodore Hailperin (Note E) in [43, pp. 44\u2013202]. English translation of \u00a7 5 with a different introduction by Heijenoort and some additional extended notes by Dreben also in [32, pp. 525\u2013581]. (Herbrand\u2019s PhD thesis, his cardinal work, dated April 14, 1929; submitted at the Univ. of Paris; defended at the Sorbonne June 11, 1930; printed in Warsaw, 1930.)"},{"key":"56_CR41","unstructured":"Herbrand, J.: Le d\u00e9veloppement moderne de la th\u00e9orie des corps alg\u00e9briques\u2014corps de classes et lois de r\u00e9ciprocit\u00e9. M\u00e9morial des Sciences Math\u00e9matiques, Fascicule LXXV, Gauthier-Villars, Paris (1936). Ed. and with an appendix by Claude Chevalley"},{"key":"56_CR42","unstructured":"Herbrand, J.: \u00c9crits logiques, Presses Universitaires de France, Paris (1968). Ed. by Jean van Heijenoort. English translation is [43]. (Herbrand\u2019s logical writings, faultily retyped)"},{"key":"56_CR43","doi-asserted-by":"crossref","unstructured":"Herbrand, J.: Logical Writings. Harvard University Press (1971). Ed. by Warren Goldfarb. Translation of [42] with additional annotations, brief introductions, and extended notes by Goldfarb, Burton Dreben, and Jean van Heijenoort. (Still the best source on Herbrand\u2019s logical writings today)","DOI":"10.1007\/978-94-010-3072-4"},{"key":"56_CR44","unstructured":"Hilbert, D., Bernays, P.: Die Grundlagen der Mathematik\u2014Erster Band. Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, no. XL. Springer, Berlin (1934). 1st edn. (2nd edn. is [46])"},{"key":"56_CR45","unstructured":"Hilbert, D., Bernays, P.: Die Grundlagen der Mathematik\u2014Zweiter Band. Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, no. L. Springer, Berlin (1939). 1st edn. (2nd edn. is [47])"},{"key":"56_CR46","unstructured":"Hilbert, D., Bernays, P.: Die Grundlagen der Mathematik I. Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, no. 40. Springer, Berlin (1968). 2nd rev. edn. of [44]"},{"key":"56_CR47","doi-asserted-by":"crossref","unstructured":"Hilbert, D., Bernays, P.: Die Grundlagen der Mathematik II. Die Grundlehren der Mathematischen Wissenschaften in Einzeldarstellungen, no. 50. Springer, Berlin (1970). 2nd rev. edn. of [45]","DOI":"10.1007\/978-3-642-86896-2"},{"key":"56_CR48","unstructured":"Hilbert, D., Bernays, P.: Grundlagen der Mathematik I\u2014Foundations of Mathematics I, Part A. College Publications, London (2011). First English translation. Commented, bilingual edition of the second eidition [46] with German facsimile, including the annotation and translation of all differences of the first German edition [46]. Translated by C.-P. Wirth. Edited by C.-P. Wirth, J. Siekmann, M. Gabbay, D. Gabbay. Advisory Board: W. Sieg (chair), I.H. Anellis, S. Awodey, M. Baaz, W. Buchholz, B. Buldt, R. Kahle, P. Mancosu, C. Parsons, V. Peckhaus, W.W. Tait, C. Tapp, R. Zach. ISBN 978-1-84890-033-2"},{"key":"56_CR49","doi-asserted-by":"crossref","unstructured":"Jaakko, K., Hintikka, J.: The Principles of Mathematics Revisited. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624919"},{"key":"56_CR50","unstructured":"Kuhn, T.S.: The Structure of Scientific Revolutions, 1st edn. University of Chicago Press (1962)"},{"key":"56_CR51","doi-asserted-by":"crossref","unstructured":"L\u00f6wenheim, L.: \u00dcber M\u00f6glichkeiten im Relativkalk\u00fcl. Math. Ann. 76, 228\u2013251 (1915). English translation: On Possibilities in the Calculus of Relatives by Stefan Bauer-Mengelberg with an introduction by Jean van Heijenoort in [32, pp. 228\u2013251]","DOI":"10.1007\/BF01458217"},{"key":"56_CR52","doi-asserted-by":"crossref","first-page":"258","DOI":"10.1145\/357162.357169","volume":"4","author":"A. Martelli","year":"1982","unstructured":"Martelli A., Montanari U.: An efficient unification algorithm. ACM Trans. Programm. Lang. Syst. 4, 258\u2013282 (1982)","journal-title":"ACM Trans. Programm. Lang. Syst."},{"key":"56_CR53","unstructured":"Menzler-Trott, E.: Gentzen\u2019s Problem\u2014Mathematische Logik im nationalsozialistischen Deutschland. Birkh\u00e4user\/Springer, Berlin (2001). Rev. English translation is [53]"},{"key":"56_CR54","unstructured":"Menzler-Trott, E.: Logic\u2019s Lost Genius\u2014The Life of Gerhard Gentzen. American Math. Soc. (2007). Rev. English translation of [52]"},{"key":"56_CR55","doi-asserted-by":"crossref","first-page":"158","DOI":"10.1016\/0022-0000(78)90043-0","volume":"16","author":"M.S. Paterson","year":"1978","unstructured":"Paterson M.S., Wegman M.N.: Linear unification. J. Comput. Syst. Sci. 16, 158\u2013167 (1978)","journal-title":"J. Comput. Syst. Sci."},{"key":"56_CR56","doi-asserted-by":"crossref","unstructured":"Peckhaus, V.: Schr\u00f6der\u2019s logic (2004). In: [23, vol. 3: The Rise of Modern Logic: From Leibniz to Frege, pp. 557\u2013610]","DOI":"10.1016\/S1874-5857(04)80022-0"},{"key":"56_CR57","doi-asserted-by":"crossref","unstructured":"Peirce, C.S.: On the algebra of logic: a contribution to the philosophy of notation. Am. J. Math. 7, 180\u2013202 (1885). Also in [58, pp. 162\u2013190]","DOI":"10.2307\/2369451"},{"key":"56_CR58","unstructured":"Peirce, C.S.: Writings of Charles S. Peirce\u2014A Chronological Edition, vol. 5, 1884\u20131886. Indiana University Press (1993). Ed. by C.J.W. Kloesel"},{"key":"56_CR59","unstructured":"Schr\u00f6der, E.: Vorlesungen \u00fcber die Algebra der Logik, vol. 3, Algebra der Logik und der Relative, Vorlesungen I-XII. B.G. Teubner Verlagsgesellschaft, Leipzig (1895). English translation of some parts in [13]"},{"key":"56_CR60","unstructured":"Sch\u00fctte, K.: Beweistheorie. Grundlehren der mathematischen Wissenschaften, no. 103. Springer, Berlin (1960). Thoroughly revised English translation: [61]"},{"key":"56_CR61","doi-asserted-by":"crossref","unstructured":"Sch\u00fctte, K.: Proof theory. Grundlehren der mathematischen Wissenschaften, no. 225. Springer, Berlin (1977). Translated from a thorough revision of [60] by J.N. Crossley","DOI":"10.1007\/978-3-642-66473-1"},{"key":"56_CR62","unstructured":"Skolem, T.: \u00dcber die mathematische Logik (Nach einem Vortrag gehalten im Norwegischen Mathematischen Verein am 22. Oktober 1928). Nordisk Matematisk Tidskrift 10, 125\u2013142 (1928). Also in [63, pp. 189\u2013206]. English translation \u201cOn Mathematical Logic\u201d by Stefan Bauer-Mengelberg and Dagfinn F\u00f8llesdal with an introduction by Burton Dreben and Jean van Heijenoort in [32, pp. 508\u2013524]. (First explicit occurrence of Skolemization and Skolem functions)"},{"key":"56_CR63","unstructured":"Skolem, T.: Selected Works in Logic. Universitetsforlaget Oslo (1970). Ed. by J.E. Fenstad. (Without index, but with most funny spellings in the newly set titles)"},{"key":"56_CR64","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-86718-7","volume-title":"First-Order Logic","author":"R.M. Smullyan","year":"1968","unstructured":"Smullyan R.M.: First-Order Logic. Springer, Berlin (1968)"},{"key":"56_CR65","unstructured":"Stern, J. (ed.): Proceedings of the Herbrand Symposium, Logic Colloquium\u201981, Marseilles, France, July 1981. North-Holland\/Elsevier (1982)"},{"key":"56_CR66","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1093\/philmat\/nkj011","volume":"14","author":"W.W. Tait","year":"2006","unstructured":"Tait W.W.: G\u00f6del\u2019s correspondence on proof theory and constructive mathematics. Philos. Math. (III) 14, 76\u2013111 (2006)","journal-title":"Philos. Math. (III)"},{"key":"56_CR67","unstructured":"Taylor, R., Wiles, A.: Ring theoretic properties of certain Hecke algebras. Ann. Math. 141, 553\u2013572 (1995). Received Oct 7, 1994. Appendix due to Gerd Faltings received Jan 26, 1995"},{"key":"56_CR68","unstructured":"Wallen, L.A.: Automated Proof Search in Non-Classical Logics. MIT Press (1990)"},{"key":"56_CR69","unstructured":"Whitehead, A.N., Russell, B.: Principia Mathematica, 1st edn. Cambridge University Press (1910\u20131913)"},{"key":"56_CR70","doi-asserted-by":"crossref","first-page":"443","DOI":"10.2307\/2118559","volume":"141","author":"A. Wiles","year":"1995","unstructured":"Wiles A.: Modular elliptic curves and Fermat\u2019s Last Theorem. Ann. Math. 141, 443\u2013551 (1995)","journal-title":"Ann. Math."},{"key":"56_CR71","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P.: Descente Infinie + Deduction. Logic J. IGPL 12, 1\u201396 (2004). http:\/\/www.ags.uni-sb.de\/~cp\/p\/d","DOI":"10.1093\/jigpal\/12.1.1"},{"key":"56_CR72","unstructured":"Wirth, C.-P.: lim+, \u03b4 +, and non-permutability of \u03b2-steps. SEKI-Report SR-2005-01 (ISSN 1437\u20134447). SEKI Publications, Saarland University (2006). Rev.edn. http:\/\/arxiv.org\/abs\/0902.3635 . Thoroughly improved version is [76]"},{"key":"56_CR73","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P.: Hilbert\u2019s epsilon as an operator of indefinite committed choice. J. Appl. Logic 6, 287\u2013317 (2008). doi: 10.1016\/j.jal.2007.07.009","DOI":"10.1016\/j.jal.2007.07.009"},{"key":"56_CR74","unstructured":"Wirth, C.-P.: Hilbert\u2019s epsilon as an operator of indefinite committed choice. SEKI-Report SR-2006-02 (ISSN 1437\u20134447). SEKI Publications, Saarland University, rev. edn. (2010). http:\/\/arxiv.org\/abs\/0902.3749"},{"key":"56_CR75","unstructured":"Wirth, C.-P.: A simplified and improved free-variable framework for Hilbert\u2019s epsilon as an operator of indefinite committed choice. SEKI Report SR-2011-01 (ISSN 1437\u20134447), SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D-28359 Bremen, Germany (2012). Rev. edn. http:\/\/arxiv.org\/abs\/1104.2444"},{"key":"56_CR76","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P.: lim+, \u03b4 +, and Non-Permutability of \u03b2-Steps. J. Symbolic Comput. 47 (2012). doi: 10.1016\/j.jsc.2011.12.035 . More funny version is [72]","DOI":"10.1016\/j.jsc.2011.12.035"},{"key":"56_CR77","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P.: Human-oriented inductive theorem proving by descente infinie\u2014a manifesto. Logic J. IGPL 20 (2012, to appear). doi: 10.1093\/jigpal\/jzr048","DOI":"10.1093\/jigpal\/jzr048"},{"key":"56_CR78","doi-asserted-by":"crossref","unstructured":"Wirth, C.-P., Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Jacques Herbrand: life, logic, and automated deduction. In: [23, vol. 5: Logic from Russell to Church, pp. 195\u2013254] (2009)","DOI":"10.1016\/S1874-5857(09)70009-3"},{"key":"56_CR79","unstructured":"Wirth, C.-P., Siekmann, J., Benzm\u00fcller, C., Autexier, S.: Lectures on Herbrand as a logician. SEKI-Report SR-2009-01 (ISSN 1437\u20134447), SEKI Publications, DFKI Bremen GmbH, Safe and Secure Cognitive Systems, Cartesium, Enrique Schmidt Str. 5, D-28359 Bremen, Germany (2011). Rev. edn. http:\/\/arxiv.org\/abs\/0902.4682"}],"container-title":["Logica Universalis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-012-0056-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11787-012-0056-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11787-012-0056-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,23]],"date-time":"2023-06-23T21:56:09Z","timestamp":1687557369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11787-012-0056-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,26]]},"references-count":79,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["56"],"URL":"https:\/\/doi.org\/10.1007\/s11787-012-0056-7","relation":{},"ISSN":["1661-8297","1661-8300"],"issn-type":[{"value":"1661-8297","type":"print"},{"value":"1661-8300","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,26]]}}}