{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T23:10:00Z","timestamp":1725491400084},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540744634"},{"type":"electronic","value":"9783540744641"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74464-1_13","type":"book-chapter","created":{"date-parts":[[2007,9,12]],"date-time":"2007-09-12T06:58:12Z","timestamp":1189580292000},"page":"188-202","source":"Crossref","is-referenced-by-count":2,"title":["A Finite First-Order Theory of Classes"],"prefix":"10.1007","author":[{"given":"Florent","family":"Kirchner","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1515\/crll.1925.154.219","volume":"154","author":"J. Neumann von","year":"1925","unstructured":"von Neumann, J.: Eine Axiomatisierung der Mengenlehre. Journal f\u00fcr die reine und angewandte Mathematik\u00a0154, 219\u2013240 (1925)","journal-title":"Journal f\u00fcr die reine und angewandte Mathematik"},{"key":"13_CR2","volume-title":"Annals of Mathematics Studies","author":"K. G\u00f6del","year":"1940","unstructured":"G\u00f6del, K.: The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory. In: Annals of Mathematics Studies, vol.\u00a03, Princeton University Press, Princeton (1940)"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bernays, P.: Axiomatic Set Theory. Dover Publications (1958)","DOI":"10.1016\/S0049-237X(08)71570-2"},{"key":"13_CR4","volume-title":"Introduction to mathematical logic","author":"E. Mendelson","year":"1997","unstructured":"Mendelson, E.: Introduction to mathematical logic, 4th edn. Chapman & Hall, Sydney (1997)","edition":"4"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-39185-1_18","volume-title":"Types for Proofs and Programs","author":"S. Vaillant","year":"2003","unstructured":"Vaillant, S.: A finite first-order presentation of set theory. In: Geuvers, H., Wiedijk, F. (eds.) TYPES 2002. LNCS, vol.\u00a02646, pp. 316\u2013330. Springer, Heidelberg (2003)"},{"key":"13_CR6","unstructured":"Kirchner, F.: Fellowship: who needs a manual anyway? (2005)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/11541868_19","volume-title":"Theorem Proving in Higher Order Logics","author":"T. Ridge","year":"2005","unstructured":"Ridge, T., Margetson, J.: A mechanically verified, sound and complete theorem prover for first order logic. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 294\u2013309. Springer, Heidelberg (2005)"},{"issue":"1","key":"13_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1017\/S0960129500003236","volume":"11","author":"G. Dowek","year":"2001","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: HOL-\u03bb\u03c3: An intentional first-order expression of higher-order logic. Mathematical Structures in Computer Science\u00a011(1), 21\u201345 (2001)","journal-title":"Mathematical Structures in Computer Science"},{"key":"13_CR9","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1145\/232627.232632","volume-title":"ICFP","author":"T. Hardin","year":"1996","unstructured":"Hardin, T., Maranget, L., Pagano, B.: Functional back-ends within the lambda-sigma calculus. In: ICFP, pp. 25\u201333. ACM Press, New York (1996)"},{"key":"13_CR10","unstructured":"Dowek, G., Miquel, A.: Cut elimination for Zermelo\u2019s set theory. Submitted to RTA 2006 (2006)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/978-3-540-32033-3_31","volume-title":"Term Rewriting and Applications","author":"G. Dowek","year":"2005","unstructured":"Dowek, G., Werner, B.: Arithmetic as a theory modulo. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 423\u2013437. Springer, Heidelberg (2005)"},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1023\/A:1027357912519","volume":"31","author":"G. Dowek","year":"2003","unstructured":"Dowek, G., Hardin, T., Kirchner, C.: Theorem proving modulo. Journal of Automated Reasoning\u00a031(1), 33\u201372 (2003)","journal-title":"Journal of Automated Reasoning"},{"key":"13_CR13","unstructured":"Lelong-Ferrand, J., Arnaudies, J.M.: Cours de Math\u00e9matiques. Tome 2\u00a0: Analyse. Dunod (1972)"},{"key":"13_CR14","unstructured":"Bourbaki, N.: \u00c9l\u00e9ments de math\u00e9matique \u2013 Th\u00e9orie des ensembles. vol. 1 \u00e0 4. Masson, Paris (1968)"},{"issue":"3","key":"13_CR15","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1305\/ndjfl\/1040149359","volume":"36","author":"N. Megill","year":"1995","unstructured":"Megill, N.: A finitely axiomatized formalization of predicate calculus with equality. Notre Dame Journal of Formal Logic\u00a036(3), 435\u2013453 (1995)","journal-title":"Notre Dame Journal of Formal Logic"},{"issue":"2","key":"13_CR16","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1023\/A:1006050629424","volume":"22","author":"J. Belinfante","year":"1999","unstructured":"Belinfante, J.: Computer proofs in G\u00f6del\u2019s class theory with equational definitions for composite and cross. Journal of Automated Reasoning\u00a022(2), 311\u2013339 (1999)","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"13_CR17","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"R. Boyer","year":"1986","unstructured":"Boyer, R., Lusk, E., McCune, W., Overbeek, R., Stickel, M., Wos, L.: Set theory in first-order logic: Clauses for G\u00f6del\u2019s axioms. Journal of Automated Reasoning\u00a02(3), 287\u2013327 (1986)","journal-title":"Journal of Automated Reasoning"},{"issue":"1","key":"13_CR18","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/BF00263451","volume":"8","author":"A. Quaife","year":"1992","unstructured":"Quaife, A.: Automated deduction in von Neumann-Bernays-G\u00f6del set theory. Journal of Automated Reasoning\u00a08(1), 91\u2013147 (1992)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Types for Proofs and Programs"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74464-1_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:30:44Z","timestamp":1619519444000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74464-1_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540744634","9783540744641"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74464-1_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}