{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:54Z","timestamp":1725559254339},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_4","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"25-34","source":"Crossref","is-referenced-by-count":1,"title":["Using a First Order Logic to Verify That Some Set of Reals Has No Lesbegue Measure"],"prefix":"10.1007","author":[{"given":"John","family":"Cowles","sequence":"first","affiliation":[]},{"given":"Ruben","family":"Gamboa","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","unstructured":"Cowles, J.: ACL2 book: Principle of dependent choices. Formal proof script available from author (2010)"},{"key":"4_CR2","unstructured":"Davis, J.: Acl2-books repository. Presented at the ACL2 Workshop (2009)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Gamboa, R., Cowles, J.: Theory extension in ACL2(r). Journal of Automated Reasoning (May 2007)","DOI":"10.1007\/s10817-006-9043-0"},{"issue":"4","key":"4_CR4","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1023\/A:1011908113514","volume":"27","author":"R. Gamboa","year":"2001","unstructured":"Gamboa, R., Kaufmann, M.: Nonstandard analysis in ACL2. Journal of Automated Reasoning\u00a027(4), 323\u2013351 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-0615-6","volume-title":"Lectures on the Hyperreals: An Introduction to Nonstandard Analysis, ch. 16","author":"R. Goldblatt","year":"1998","unstructured":"Goldblatt, R.: Lectures on the Hyperreals: An Introduction to Nonstandard Analysis, ch. 16. Springer, Heidelberg (1998)"},{"key":"4_CR6","volume-title":"The Axiom of Choice","author":"T.J. Jech","year":"1973","unstructured":"Jech, T.J.: The Axiom of Choice, vol.\u00a075. North-Holland Publishing Company, Amsterdam (1973)"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. Journal of Automated Reasoning\u00a026(2), 161\u2013203 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1090\/S0002-9904-1977-14398-X","volume":"83","author":"E. Nelson","year":"1977","unstructured":"Nelson, E.: Internal set theory: A new approach to nonstandard analysis. Bulletin of the American Mathematical Society\u00a083, 1165\u20131198 (1977)","journal-title":"Bulletin of the American Mathematical Society"},{"key":"4_CR9","volume-title":"Real Analysis","author":"H.L. Royden","year":"1968","unstructured":"Royden, H.L.: Real Analysis, 2nd edn. Macmillan, Basingstoke (1968)","edition":"2"},{"key":"4_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2307\/1970696","volume":"92","author":"R.M. Solovay","year":"1970","unstructured":"Solovay, R.M.: A model of set theory in which every set of reals is Lebesgue measurable. Annals of Mathematics\u00a092, 1\u201356 (1970)","journal-title":"Annals of Mathematics"},{"key":"4_CR11","unstructured":"Vitali, G.: Sul problema della mesura dei gruppi di una retta (1905)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:25Z","timestamp":1619785045000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}