{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:31Z","timestamp":1725488611586},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540671909"},{"type":"electronic","value":"9783540465089"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46508-1_1","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T16:02:03Z","timestamp":1186156923000},"page":"1-22","source":"Crossref","is-referenced-by-count":2,"title":["Automated Theorem Proving in First-Order Logic Modulo: On the Difference between Type Theory and Set Theory"],"prefix":"10.1007","author":[{"given":"Gilles","family":"Dowek","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,5,17]]},"reference":[{"issue":"3","key":"1_CR1","doi-asserted-by":"publisher","first-page":"414","DOI":"10.2307\/2269949","volume":"36","author":"P.B. Andrews","year":"1971","unstructured":"P.B. Andrews. Resolution in type theory. The Journal of Symbolic Logic, 36,3 (1971), pp. 414\u2013432.","journal-title":"The Journal of Symbolic Logic"},{"key":"1_CR2","unstructured":"P.B. Andrews, An introduction to mathematical logic and type theory: to truth through proof, Academic Press (1986)."},{"key":"1_CR3","unstructured":"P.B. Andrews, D.A. Miller, E. Longini Cohen, and F. Pfenning, Automating higher-order logic, W.W. Bledsoe and D.W. Loveland (Eds.), Automated theorem proving: after 25 years, Contemporary Mathematics Series 29, American Mathematical Society (1984), pp. 169\u2013192."},{"issue":"3","key":"1_CR4","doi-asserted-by":"publisher","first-page":"673","DOI":"10.2307\/2274565","volume":"53","author":"S.C. Bailin","year":"1988","unstructured":"S.C. Bailin, A normalization theorem for set theory, The Journal of Symbolic Logic, 53,3 (1988), pp. 673\u2013695.","journal-title":"The Journal of Symbolic Logic"},{"key":"1_CR5","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1007\/BF00244943","volume":"4","author":"S.C. Bailin","year":"1988","unstructured":"S.C. Bailin, A \u03bb-unifiability test for set theory, Journal of Automated Reasoning, 4 (1988), pp. 269\u2013286.","journal-title":"Journal of Automated Reasoning"},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, 5 (1940), pp. 56\u201368.","journal-title":"The Journal of Symbolic Logic"},{"key":"1_CR7","unstructured":"M. Davis, Invited commentary to [28], A.J.H. Morrell (Ed.) Proceedings of the International Federation for Information Processing Congress, 1968, North Holland (1969) pp. 67\u201368."},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/0304-3975(93)90075-5","volume":"114","author":"D.J. Dougherty","year":"1993","unstructured":"D.J. Dougherty, Higher-order unification via combinators, Theoretical Computer Science, 114 (1993), pp. 273\u2013298.","journal-title":"Theoretical Computer Science"},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/BFb0014051","volume-title":"Typed Lambda Calculi and Applications","author":"G. Dowek","year":"1995","unstructured":"G. Dowek, Lambda-calculus, combinators and the comprehension scheme, M. Dezani-Ciancaglini and G. Plotkin (Eds.), Typed Lambda Calculi and Applications, Lecture notes in computer science 902, Springer-Verlag (1995), pp. 154\u2013170. Rapport de Recherche 2565, INRIA (1995)."},{"key":"1_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BFb0028389","volume-title":"Theorem Proving in Higher-order Logics","author":"G. Dowek","year":"1997","unstructured":"G. Dowek, Proof normalization for a first-order formulation of higher-order logic, E.L. Gunter and A. Felty (Eds.), Theorem Proving in Higher-order Logics, Lecture notes in computer science 1275, Springer-Verlag (1997), pp. 105\u2013119. Rapport de Recherche 3383, INRIA (1998)."},{"key":"1_CR11","unstructured":"G. Dowek, Th. Hardin, and C. Kirchner, Theorem proving modulo, Rapport de Recherche 3400, INRIA (1998)."},{"key":"1_CR12","unstructured":"G. Dowek, Th. Hardin, and C. Kirchner, HOL-\u03bb\u03c3: an intentional first-order expression of higher-order logic, to appear in Rewriting Techniques and Applications (1999). Rapport de Recherche 3556, INRIA (1998)."},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"G. Dowek and B. Werner, Proof normalization modulo, Rapport de Recherche 3542, INRIA (1998).","DOI":"10.1007\/3-540-48167-2_5"},{"key":"1_CR14","unstructured":"J. Ekman, Normal proofs in set theory, Doctoral thesis, Chalmers University of Technology and University of G\u00f6teborg (1994)."},{"key":"1_CR15","unstructured":"M. Fay, First-order unification in an equational theory, Fourth Workshop on Automated Deduction (1979), pp. 161\u2013167."},{"key":"1_CR16","unstructured":"L. Halln\u00e4s, On normalization of proofs in set theory, Doctoral thesis, University of Stockholm (1983)."},{"key":"1_CR17","unstructured":"G. Huet, Constrained resolution: a complete method for higher order logic, Ph.D., Case Western Reserve University (1972)."},{"key":"1_CR18","unstructured":"G. Huet, A mechanization of type theory, International Joint Conference on Artificial Intelligence (1973), pp. 139\u2013146."},{"issue":"1","key":"1_CR19","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. Huet","year":"1975","unstructured":"G. Huet, A unification algorithm for typed lambda calculus, Theoretical Computer Science, 1,1 (1975), pp. 27\u201357.","journal-title":"Theoretical Computer Science"},{"key":"1_CR20","unstructured":"G. Huet, R\u00e9solution d\u2019\u00e9quations dans les Langages d\u2019Ordre 1,2,..., \u03c9, Th\u00e8se d\u2019 \u00c9tat, Universit\u00e9 de Paris VII (1976)."},{"key":"1_CR21","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"318","DOI":"10.1007\/3-540-10009-1_25","volume-title":"Conference on Automated Deduction","author":"J.-M. Hullot","year":"1980","unstructured":"J.-M. Hullot, Canonical forms and unification, W. Bibel and R. Kowalski (Eds.) Conference on Automated Deduction, Lecture Notes in Computer Science 87, Springer-Verlag (1980), pp. 318\u2013334."},{"key":"1_CR22","unstructured":"J.-P. Jouannaud and C. Kirchner, Solving equations in abstract algebras: a rulebased survey of unification, J.-L. Lassez and G. Plotkin (Eds.) Computational logic. Essays in honor of Alan Robinson, MIT press (1991), pp. 257\u2013321."},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1016\/0304-3975(93)90091-7","volume":"121","author":"J.W. Klop","year":"1993","unstructured":"J.W. Klop, V. van Oostrom, and F. van Raamsdonk, Combinatory reduction systems: introduction and survey, Theoretical Computer Science, 121 (1993), pp. 279\u2013308.","journal-title":"Theoretical Computer Science"},{"key":"1_CR24","unstructured":"D.A. Miller, Proofs in higher order logic, Ph.D., Carnegie Mellon University (1983)."},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"D.A. Miller, A compact representation of proofs, Studia Logica, 46,4 (1987).","DOI":"10.1007\/BF00370646"},{"key":"1_CR26","first-page":"73","volume":"7","author":"G. Plotkin","year":"1972","unstructured":"G. Plotkin, Building-in equational theories, Machine Intelligence, 7 (1972), pp. 73\u201390.","journal-title":"Machine Intelligence"},{"key":"1_CR27","unstructured":"W.V.O. Quine, Set theory and its logic, Belknap press (1969)."},{"key":"1_CR28","unstructured":"J.A. Robinson. New directions in mechanical theorem proving. A.J.H. Morrell (Ed.) Proceedings of the International Federation for Information Processing Congress, 1968, North Holland (1969), pp. 63\u201367."},{"key":"1_CR29","first-page":"123","volume":"5","author":"J.A. Robinson","year":"1970","unstructured":"J.A. Robinson. A note on mechanizing higher order logic. Machine Intelligence 5, Edinburgh university press (1970), pp. 123\u2013133.","journal-title":"Machine Intelligence"},{"issue":"1","key":"1_CR30","first-page":"285","volume":"4","author":"M. Stickel","year":"1985","unstructured":"M. Stickel, Automated deduction by theory resolution, Journal of Automated Reasoning, 4,1 (1985), pp. 285\u2013289.","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction in Classical and Non-Classical Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46508-1_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T14:57:53Z","timestamp":1556722673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46508-1_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540671909","9783540465089"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/3-540-46508-1_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}