{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:58Z","timestamp":1774984078343,"version":"3.50.1"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,4,2]],"date-time":"2015-04-02T00:00:00Z","timestamp":1427932800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10817-015-9322-8","type":"journal-article","created":{"date-parts":[[2015,4,3]],"date-time":"2015-04-03T01:26:32Z","timestamp":1428024392000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":26,"title":["A Mechanised Proof of G\u00f6del\u2019s Incompleteness Theorems Using Nominal Isabelle"],"prefix":"10.1007","volume":"55","author":[{"given":"Lawrence C.","family":"Paulson","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,2]]},"reference":[{"issue":"3","key":"9322_CR1","first-page":"5","volume":"22","author":"J Bagaria","year":"2003","unstructured":"Bagaria, J.: A short guide to G\u00f6del\u2019s second incompleteness theorem. Teorema 22(3), 5\u201315 (2003)","journal-title":"Teorema"},{"key":"9322_CR2","doi-asserted-by":"crossref","unstructured":"Boolos, G.S.: The logic of provability, Cambridge University Press (1993)","DOI":"10.1017\/CBO9780511625183"},{"key":"9322_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"NG Bruijn de","year":"1972","unstructured":"de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indag. Math. 34, 381\u2013392 (1972)","journal-title":"Indag. Math."},{"key":"9322_CR4","unstructured":"Feferman, S. (ed.): Kurt G\u00f6del, Collected Works, volume I. Oxford University Press (1986)"},{"key":"9322_CR5","doi-asserted-by":"crossref","unstructured":"Franz\u00e9n, T.: G\u00f6del\u2019s theorem: An incomplete guide to its use and abuse. A K Peters (2005)","DOI":"10.1201\/b10700"},{"key":"9322_CR6","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/s001650200016","volume":"13","author":"MJ Gabbay","year":"2001","unstructured":"Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax with variable binding. Form. Asp. Comput. 13, 341\u2013363 (2001)","journal-title":"Form. Asp. Comput."},{"key":"9322_CR7","unstructured":"G\u00f6del, K.: On completeness and consistency. In: Feferman 4, pp 234\u2013236"},{"key":"9322_CR8","unstructured":"G\u00f6del, K.: On formally undecidable propositions of Principia Mathematica and related systems. In: Feferman 4, pp. 144\u2013195. First published in 1931 in the Monatshefte f\u00fcr Mathematik und Physik (1931)"},{"key":"9322_CR9","doi-asserted-by":"crossref","unstructured":"Grandy, R.E.: Advanced Logic for Applications. Reidel (1977)","DOI":"10.1007\/978-94-010-1191-4"},{"key":"9322_CR10","unstructured":"Harrison, J.: Re: G\u00f6del\u2019s incompleteness theorem, Email dated 15 January (2014)"},{"key":"9322_CR11","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Towards self-verification of HOL Light. In: Furbach, U., Shankar, N. (eds.) Automated Reasoning \u2014 Third International Joint Conference, IJCAR, 2006, LNAI 4130, pp. 177\u2013191. Springer (2006)","DOI":"10.1007\/11814771_17"},{"key":"9322_CR12","doi-asserted-by":"crossref","unstructured":"Harrison, J.: Handbook of Practical Logic and Automated Reasoning. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511576430"},{"key":"9322_CR13","unstructured":"Richard, E.H.: An Introduction to Mathematical Logic. PWS Publishing Company (1995)"},{"key":"9322_CR14","doi-asserted-by":"crossref","unstructured":"Hurd, J., Melham, T.: Theorem Proving in Higher Order Logics: TPHOLs 2005, LNCS 3603. Springer (2005)","DOI":"10.1007\/11541868"},{"issue":"1","key":"9322_CR15","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1002\/malq.200610026","volume":"53","author":"L Kirby","year":"2007","unstructured":"Kirby, L.: Addition and multiplication of sets. Math. Logic Q. 53(1), 52\u201365 (2007)","journal-title":"Math. Logic Q."},{"key":"9322_CR16","unstructured":"Kunen, K.: Set Theory : An Introduction to Independence Proofs. North-Holland (1980)"},{"key":"9322_CR17","doi-asserted-by":"crossref","unstructured":"Lochbihler, A.: Formalising finfuns \u2014 generating code for functions as data from Isabelle\/HOL. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs, vol. 5674 of Lecture Notes in Computer Science, pp. 310\u2013326. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_22"},{"key":"9322_CR18","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: More Church-Rosser proofs (in Isabelle\/HOL). J. Autom. Reason. 26, 51\u201366 (2001)","DOI":"10.1023\/A:1006496715975"},{"key":"9322_CR19","doi-asserted-by":"crossref","unstructured":"Nipkow T., Lawrence, C. P.: Proof pearl: Defining functions over finite sets. In: Hurd and Melham 14, pp. 385\u2013396.","DOI":"10.1007\/11541868_25"},{"key":"9322_CR20","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer. An up-to-date version is distributed with Isabelle (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9322_CR21","doi-asserted-by":"crossref","unstructured":"Norrish, M., Vestergaard, R.: Proof pearl: de Bruijn terms really do work. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics: TPHOLs 2007, LNCS 4732, pp. 207\u2013222. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_16"},{"key":"9322_CR22","unstructured":"O\u2019Connor, R.: Essential incompleteness of arithmetic verified by Coq. In Hurd and Melham 14"},{"key":"9322_CR23","unstructured":"Russell, S.S.: O\u2019Connor. Incompleteness & Completeness: Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud University Nijmegen (2009)"},{"issue":"3","key":"9322_CR24","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1007\/BF00881873","volume":"11","author":"C Lawrence","year":"1993","unstructured":"Lawrence, C.: Paulson. Set theory for verification: I. From foundations to functions. J. Autom. Reas. 11(3), 353\u2013389 (1993)","journal-title":"J. Autom. Reas."},{"key":"9322_CR25","doi-asserted-by":"crossref","first-page":"198","DOI":"10.1112\/S1461157000000449","volume":"6","author":"LC Paulson","year":"2003","unstructured":"Paulson, L.C.: The relative consistency of the axiom of choice \u2014 mechanized using Isabelle\/ZF. LMS J. Comput. Math. 6, 198\u2013248 (2003). http:\/\/www.lms.ac.uk\/jcm\/6\/lms2003-001\/","journal-title":"LMS J. Comput. Math."},{"key":"9322_CR26","unstructured":"Paulson, L.C.: G\u00f6del\u2019s incompleteness theorems. Archive of Formal Proofs. November. Formal proof development. (2013). http:\/\/afp.sf.net\/entries\/Incompleteness.shtml"},{"issue":"3","key":"9322_CR27","doi-asserted-by":"crossref","first-page":"484","DOI":"10.1017\/S1755020314000112","volume":"7","author":"LC Paulson","year":"2014","unstructured":"Paulson, L.C.: A machine-assisted proof of G\u00f6del\u2019s incompleteness theorems for the theory of hereditarily finite sets. Rev. Symb. Log. 7(3), 484\u2013498 (2014)","journal-title":"Rev. Symb. Log."},{"key":"9322_CR28","doi-asserted-by":"crossref","unstructured":"Pitts, A.M.: Nominal sets names and symmetry in computer science. Cambridge University Press (2013)","DOI":"10.1017\/CBO9781139084673"},{"key":"9322_CR29","unstructured":"Shankar, N.: Proof-checking Metamathematics. PhD thesis, University of Texas at Austin (1986)"},{"key":"9322_CR30","doi-asserted-by":"crossref","unstructured":"Shankar, N.: Metamathematics Machines, and G\u00f6del\u2019s Proof. Cambridge University Press (1994)","DOI":"10.1017\/CBO9780511569883"},{"key":"9322_CR31","unstructured":"Shankar, N., Shankar, B.: Church-Rosser and de Bruijn indices. E-mail (2013)"},{"key":"9322_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4064\/dm422-0-1","volume":"422","author":"S \u015awierczkowski","year":"2003","unstructured":"\u015awierczkowski, S.: Finite sets and Godel\u2019s\u0308 incompleteness theorems. Dissertationes Mathematicae 422, 1\u201358 (2003). http:\/\/journals.impan.gov.pl\/dm\/Inf\/422-0-1.html","journal-title":"Dissertationes Mathematicae"},{"key":"9322_CR33","doi-asserted-by":"crossref","unstructured":"Urban, C.: Nominal techniques in Isabelle\/HOL. J. Autom. Reason. 40(4), 327\u2013356 (2008)","DOI":"10.1007\/s10817-008-9097-2"},{"issue":"2:14","key":"9322_CR34","first-page":"1","volume":"8","author":"C Urban","year":"2012","unstructured":"Urban, C., Kaliszyk, C.: General bindings and alpha-equivalence in Nominal Isabelle. Log. Methods Comput. Sci. 8(2:14), 1\u201335 (2012)","journal-title":"Log. Methods Comput. Sci."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9322-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9322-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9322-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,22]],"date-time":"2019-08-22T17:08:06Z","timestamp":1566493686000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9322-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,2]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["9322"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9322-8","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,2]]}}}