{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,28]],"date-time":"2022-12-28T20:28:42Z","timestamp":1672259322754},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"1","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\/bf00881863","type":"journal-article","created":{"date-parts":[[2004,12,27]],"date-time":"2004-12-27T07:34:31Z","timestamp":1104132871000},"page":"15-58","source":"Crossref","is-referenced-by-count":11,"title":["Experimenting with Isabelle in ZF set theory"],"prefix":"10.1007","volume":"10","author":[{"given":"P. A. J.","family":"Noel","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","unstructured":"Aczel, Peter,Non-Well-Founded Sets, CSLI Lecture Notes 14 (1988)."},{"key":"CR2","unstructured":"Andrews, Peter B.,An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, Academic Press (1986)."},{"key":"CR3","unstructured":"Borzyszkowski, A., Kubiak, R., Leszczylowski, J., and Sokolowski, S., ?Towards a set-theoretic type theory?, Technical report, Institute of Computer Science, Polish Academy of Sciences (September 1988)."},{"key":"CR4","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, 287?327 (1986).","journal-title":"J. Automated Reasoning"},{"key":"CR5","unstructured":"Corella, Francisco, ?Mechanising set theory?, Technical Report RC 14706 (*65927), IBM Research Division (1989)."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Gabbay, D. and Guenthner, F. (Eds.),Handbook of Philosophical Logic, D. Reidel Publishing Company (1983).","DOI":"10.1007\/978-94-009-7066-3"},{"key":"CR7","doi-asserted-by":"crossref","unstructured":"Gordon, Michael J. C., Milner, Robin, and Wadsworth, Christopher P.,Edinburgh LCF: A Mechanised Logic of Computation, Springer-Verlag (1979). LNCS 78.","DOI":"10.1007\/3-540-09724-4"},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Hamilton, A. G.,Numbers, Sets and Axioms, Pergamon Press (1982).","DOI":"10.1017\/CBO9781139171618"},{"key":"CR9","unstructured":"Hatcher, William S.,The Logical Foundations of Mathematics, Pergamon Press (1982)."},{"key":"CR10","volume-title":"Introduction to Combinators and ?-Calculus","author":"J. Roger Hindley","year":"1986","unstructured":"Hindley, J. Roger and Seldin, Jonathon P.,Introduction to Combinators and ?-Calculus, Cambridge, University Press (1986)."},{"key":"CR11","unstructured":"Huet, G. P., ?Induction principles formalised in the calculus of constructions?, in:TAPSOFT 87, pp. 276?286, Springer-Verlag (1987). LNCS 249."},{"key":"CR12","doi-asserted-by":"crossref","unstructured":"Paulson, Lawrence C.,Logic and Computation: Interactive Proof with Cambridge LCF, Cambridge University Press (1987).","DOI":"10.1017\/CBO9780511526602"},{"key":"CR13","unstructured":"Paulson, Lawrence C., ?A preliminary user's manual for Isabelle?, Technical Report 133, University of Cambridge Computer Laboratory (1988)."},{"key":"CR14","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, 363?397 (1989).","journal-title":"J. Automated Reasoning"},{"key":"CR15","unstructured":"Paulson, Lawrence C. and Nipkow, Tobias, ?Isabelle tutorial and user's manual?, Technical Report 189, University of Cambridge Computer Laboratory (1990)."},{"key":"CR16","doi-asserted-by":"crossref","unstructured":"Sundholm, Goran, ?Systems of deduction?, in [6], Vol. 1, pp. 133?188 (1983).","DOI":"10.1007\/978-94-009-7066-3_2"},{"key":"CR17","unstructured":"Suppes, Patrick,Axiomatic Set Theory, Dover (1972)."},{"key":"CR18","unstructured":"Takeuti, G.,Proof Theory, North-Holland, 2nd edn. (1987)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881863.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00881863\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00881863","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T23:53:53Z","timestamp":1586044433000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00881863"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"references-count":18,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993]]}},"alternative-id":["BF00881863"],"URL":"https:\/\/doi.org\/10.1007\/bf00881863","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993]]}}}