{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,7]],"date-time":"2025-10-07T14:28:42Z","timestamp":1759847322086},"reference-count":54,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,1,1]],"date-time":"1993-01-01T00:00:00Z","timestamp":725846400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/bf00881873","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T23:44:45Z","timestamp":1104191085000},"page":"353-389","source":"Crossref","is-referenced-by-count":58,"title":["Set theory for verification: I. From foundations to functions"],"prefix":"10.1007","volume":"11","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"CR1","unstructured":"Aczel, Peter,Non-Well-Founded Sets, CSLI (1988)."},{"key":"CR2","doi-asserted-by":"crossref","unstructured":"Andrews, Peter B., Miller, Dale A., Cohen, Eve L. and Pfenning, Frank, ?Automating higher-order logic?, in W. W. Bledsoe and D. W. Loveland (Eds.),Automated Theorem Proving: After 25 Years, pp. 169?192, American Mathematical Society (1984).","DOI":"10.1090\/conm\/029\/09"},{"issue":"3","key":"CR3","first-page":"269","volume":"4","author":"Sidney C. Bailin","year":"1988","unstructured":"Bailin, Sidney C., ?A ?-unifiability test for set theory?,J. Automated Reasoning,4(3), 269?286 (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR4","unstructured":"Bailin, Sidney C. and Barker-Plummer, Dave, ??-match: An inference rule for incrementally elaborating set instantiations?, Technical report, Swarthmore College, second revision (1993)."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Basin, David and Kaufmann, Matt, ?The Boyer-Moore prover and Nuprl: An experimental comparison?, in G\u00e9rard Huet and Gordon Plotkin (Eds.),Logical Frameworks, pp. 89?119, Cambridge University Press (1991).","DOI":"10.1017\/CBO9780511569807.006"},{"key":"CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(77)90012-1","volume":"9","author":"W. W. Bledsoe","year":"1977","unstructured":"Bledsoe, W. W., ?Non-resolution theorem proving?,Artificial Intelligence,9 1?35 (1977).","journal-title":"Artificial Intelligence"},{"key":"CR7","unstructured":"Bledsoe, W. W., ?A maximal method for set variables in automatic theorem-proving?, in J. E. Hayes, D. Michie, and L. I. Mikulich (Eds.),Machine Intelligence 9, pp. 53?100, Ellis Horwood Ltd (1979)."},{"key":"#cr-split#-CR8.1","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W. and Feng, Guohui, ?Set-var?, Technical report, University of Texas at Austin, March (1993);","DOI":"10.1007\/BF00881869"},{"key":"#cr-split#-#cr-split#-CR8.2.1","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W. and Feng, Guohui, ?Set-var?, Technical report, University of Texas at Austin, March (1993);","DOI":"10.1007\/BF00881869"},{"key":"#cr-split#-#cr-split#-CR8.2.2","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W. and Feng, Guohui, ?Set-var?, Technical report, University of Texas at Austin, March (1993);J. Automated Reasoning (forthcoming).","DOI":"10.1007\/BF00881869"},{"issue":"3","key":"CR9","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1007\/BF02328452","volume":"2","author":"Boyer","year":"1986","unstructured":"Boyer, Robert, Lusk, Ewing, McCune, William, Overbeek, Ross, Stickel, Mark and Wos, Lawrence, ?Set theory in first-order logic: Clauses for G\u00f6del's axioms?,J. Automated Reasoning,2(3), 287?327 (1986).","journal-title":"J. Automated Reasoning"},{"key":"CR10","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1016\/S0004-3702(78)80017-4","volume":"10","author":"Brown","year":"1978","unstructured":"Brown, Frank Malloy, ?Toward the automation of set theory and its logic?,Artificial Intelligence,10 281?316 (1978).","journal-title":"Artificial Intelligence"},{"issue":"2","key":"CR11","first-page":"193","volume":"7","author":"D. Cantone","year":"1991","unstructured":"Cantone, D., ?Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators?,J. Automated Reasoning,7(2), 193?230 (1991).","journal-title":"J. Automated Reasoning"},{"key":"CR12","unstructured":"Claesen, L. J. M. and Gordon, M. J. C., (Eds.),Higher Order Logic Theorem Proving and Its Applications, North-Holland (1993)."},{"key":"CR13","unstructured":"Corella, Francisco, ?Mechanizing set theory?, Technical Report RC 14706 (#65927), IBM Watson Research Center (1989)."},{"key":"CR14","doi-asserted-by":"crossref","unstructured":"Devlin, Keith J.,Fundamentals of Contemporary Set Theory, Springer (1979).","DOI":"10.1007\/978-1-4684-0084-7"},{"key":"CR15","doi-asserted-by":"crossref","unstructured":"Felty, Amy, ?A logic program for transforming sequent proofs to natural deduction proofs?, in Peter Schroeder-Heister (Ed.),Extensions of Logic Programming, pp. 157?178, Springer (1991). LNAI 475.","DOI":"10.1007\/BFb0038694"},{"key":"CR16","unstructured":"Givan, R., McAllester, D., Witty, C. and Zalondek, K., ?Ontic: Language specification and user's manual?, Technical report, MIT, 1992. Draft 4."},{"key":"CR17","unstructured":"G\u00f6del, Kurt, ?The consistency of the axiom of choice and of the generalized continuum hypothesis with the axioms of set theory?, In S. Fefermanet al. (Eds.),Kurt G\u00f6del: Collected Works, Vol. II, Oxford University Press (1990). Paper first published in 1940."},{"key":"CR18","unstructured":"Gordon, Michael J. C., ?Why higher-order logic is a good formalism for specifying and verifying hardware?, in G. Milne and P. A. Subrahmanyam (Eds.),Formal Aspects of VLSI Design, pp. 153?177, North-Holland (1986)."},{"key":"CR19","doi-asserted-by":"crossref","unstructured":"Gordon, Michael J. C., ?HOL: A proof generating system for higher-order logic?, in Graham Birtwistle and P. A. Subrahmanyam (Eds.),VLSI Specification, Verification and Synthesis, pp. 73?128, Kluwer Academic Publishers (1988).","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"CR20","doi-asserted-by":"crossref","unstructured":"Graham, Brian T.,The SECD Microprocessor: A Verification Case Study, Kluwer Academic Publishers (1992).","DOI":"10.1007\/978-1-4615-3576-8"},{"key":"CR21","unstructured":"Halmos, Paul R.,Naive Set Theory, Van Nostrand (1960)."},{"key":"CR22","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/0304-3975(75)90011-0","volume":"1","author":"G. P. Huet","year":"1975","unstructured":"Huet, G. P., ?A unification algorithm for typed ?-calculus?,Theor. Computer Sci.,1 27?57 (1975).","journal-title":"Theor. Computer Sci."},{"issue":"3","key":"CR23","doi-asserted-by":"crossref","first-page":"355","DOI":"10.1007\/BF00245295","volume":"9","author":"Kaufmann","year":"1992","unstructured":"Kaufmann, Matt, ?An extension of the Boyer-Moore theorem prover to support first-order quantification?,J. Automated Reasoning,9(3), 355?372 (1992).","journal-title":"J. Automated Reasoning"},{"key":"CR24","unstructured":"Kunen, Kenneth,Set Theory: An Introduction to Independence Proofs, North-Holland (1980)."},{"key":"CR25","unstructured":"Lamport, Leslie, ?The temporal logic of actions?, Technical report, DEC Systems Research Center (1991)."},{"key":"CR26","unstructured":"Lamport, Leslie, ?Types considered harmful?, Technical report, DEC Systems Research Center (1992). Draft."},{"key":"CR27","unstructured":"Leclerc, F. and Paulin-Mohring, Ch., ?Programming with streams in Coq. A case study: the sieve of Eratosthenes?, in B. Nordstr\u00f6m, K. Petersson, and G. Plotkin (Eds.),Workshop of Types for Proofs and Programs, pp. 245?261 (June, 1992). B\u00e5stad, Sweden."},{"key":"CR28","unstructured":"McCarty, David C., ?Realizability and recursive mathematics?, Technical Report CMU-CS-84-131, Carnegie-Mellon University (1984)."},{"key":"CR29","doi-asserted-by":"crossref","unstructured":"McDonald, James and Suppes, Patrick, ?Student use of an interactive theorem prover?, in W. W. Bledsoe and D. W. Loveland (Eds.),Automated Theorem Proving: After 25 Years, pp. 315?360, American Mathematical Society (1984).","DOI":"10.1090\/conm\/029\/16"},{"issue":"4","key":"CR30","doi-asserted-by":"crossref","first-page":"321","DOI":"10.1016\/0747-7171(92)90011-R","volume":"14","author":"Dale Miller","year":"1992","unstructured":"Miller, Dale, ?Unification under a mixed prefix?,J. Symbolic Computation,14(4), 321?358 (1992).","journal-title":"J. Symbolic Computation"},{"key":"CR31","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1093\/comjnl\/34.1.34","volume":"34","author":"Tobias Nipkow","year":"1991","unstructured":"Nipkow, Tobias, ?Constructive rewriting?,Computer J.,34 34?41 (1991).","journal-title":"Computer J."},{"issue":"1","key":"CR32","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/BF00881863","volume":"10","author":"Philippe No\u00ebl","year":"1993","unstructured":"No\u00ebl, Philippe, ?Experimenting with Isabelle in ZF set theory,J. Automated Reasoning,10(1), 15?58 (1993).","journal-title":"J. Automated Reasoning"},{"key":"CR33","unstructured":"Nordstr\u00f6m, Bengt, Petersson, Kent and Smith, Jan,Programming in Martin-L\u00f6f's Type Theory. An Introduction, Oxford University Press (1990)."},{"key":"CR34","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0004-3702(78)90028-0","volume":"10","author":"Dominque Pastre","year":"1978","unstructured":"Pastre, Dominque, ?Automatic theorem proving in set theory?,Artificial Intelligence,10 1?27 (1978).","journal-title":"Artificial Intelligence"},{"issue":"3","key":"CR35","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/BF00248324","volume":"5","author":"Lawrence C. Paulson","year":"1989","unstructured":"Paulson, Lawrence C., ?The foundation of a generic theorem prover?,J. Automated Reasoning,5(3), 363?397 (1989).","journal-title":"J. Automated Reasoning"},{"key":"CR36","unstructured":"Paulson, Lawrence C., ?Isabelle: The next 700 theorem provers?, in P. Odifreddi (Ed.),Logic and Computer Science, pp. 361?386, Academic Press (1990)."},{"key":"CR37","unstructured":"Paulson, Lawrence C., ?Introduction to Isabelle?, Technical Report 280, University of Cambridge Computer Laboratory (1993)."},{"key":"CR38","unstructured":"Paulson, Lawrence C., ?The Isabelle reference manual?, Technical Report 283, University of Cambridge Computer Laboratory (1993)."},{"key":"CR39","unstructured":"Paulson, Lawrence C., ?Isabelle's object-logics?, Technical Report 286, University of Cambridge Computer Laboratory (1993)."},{"key":"CR40","unstructured":"Paulson, Lawrence C., ?Set theory for verification: II. Induction and recursion?, Technical Report 312, University of Cambridge Computer Laboratory (1993)."},{"key":"CR41","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"Pelletier, F. J., ?Seventy-five problems for testing automatic theorem provers?,J. Automated Reasoning,2 191?216 (1986). Errata,Loc. cit.,4, 235?236 (1988).","journal-title":"J. Automated Reasoning"},{"key":"CR42","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/S0747-7171(08)80136-8","volume":"11","author":"David A. Plaisted","year":"1991","unstructured":"Plaisted, David A. and Potter, Richard C., ?Term rewriting: Some experimental results?,J. Symbolic Computation,11 149?180 (1991).","journal-title":"J. Symbolic Computation"},{"key":"CR43","doi-asserted-by":"crossref","unstructured":"Prawitz, Dag, ?Ideas and results in proof theory?, in J. E. Fenstad (Ed.),Proceedings of the Second Scandinavian Logic Symposium, pp. 235?308, North Holland (1971).","DOI":"10.1016\/S0049-237X(08)70849-8"},{"issue":"1","key":"CR44","first-page":"91","volume":"8","author":"Art Quaife","year":"1992","unstructured":"Quaife, Art, ?Automated deduction in von Neumann-Bernays-G\u00f6del set theory,J. Automated Reasoning,8(1), 91?147 (1992).","journal-title":"J. Automated Reasoning"},{"key":"CR45","doi-asserted-by":"crossref","unstructured":"Ryser, Herbert John,Combinatorial Mathematics, Mathematical Association of America (1963).","DOI":"10.5948\/UPO9781614440147"},{"key":"CR46","series-title":"Technical Report","volume-title":"TheEves library","author":"Mark Saaltink","year":"1992","unstructured":"Saaltink, Mark, ?TheEves library?, Technical Report TR-91-5449-03, ORA Canada, 265 Carling Avanue, Suite 506, Ottawa, Ontario (1992)."},{"key":"CR47","series-title":"Technical Report","volume-title":"TheEves library models","author":"Mark Saaltink","year":"1992","unstructured":"Saaltink, Mark, ?TheEves library models?, Technical Report TR-91-5449-04, ORA Canada, 265 Carling Avanue, Suite 506, Ottawa, Ontario (1992)."},{"key":"CR48","doi-asserted-by":"crossref","unstructured":"Saaltink, Mark, Kromodimoeljo, Sentot, Pase, Bill, Craigen, Dan and Meisels, Irwin, ?AnEves data abstraction example?, in J. C. P. Woodcock and P. G. Larsen (Eds.),FME '93: Industrial-Strength Formal Methods, pp. 578?596, Springer (1993), LNCS 670.","DOI":"10.1007\/BFb0024668"},{"key":"CR49","unstructured":"Schmidt, David, ?Natural deduction theorem proving in set theory?, Technical Report CSR-142-83, Department of Computer Science, University of Edinburgh (1983)."},{"key":"CR50","doi-asserted-by":"crossref","unstructured":"Shoenfield, J. R., ?Axioms of set theory?, in J. Barwise (Ed.),Handbook of Mathematical Logic, pp. 321?344, North-Holland (1977).","DOI":"10.1016\/S0049-237X(08)71106-6"},{"key":"CR51","unstructured":"Suppes, Patrick,Axiomatic Set Theory, Dover (1972)."},{"key":"CR52","unstructured":"Thompson, Simon,Type Theory and Functional Programming, Addison-Wesley (1991)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881873.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881873\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881873","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,5]],"date-time":"2020-04-05T00:16:35Z","timestamp":1586045795000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881873"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":54,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881873"],"URL":"https:\/\/doi.org\/10.1007\/bf00881873","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}