{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T19:07:48Z","timestamp":1774984068049,"version":"3.50.1"},"reference-count":9,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1986,9,1]],"date-time":"1986-09-01T00:00:00Z","timestamp":525916800000},"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":[[1986,9]]},"DOI":"10.1007\/bf02328452","type":"journal-article","created":{"date-parts":[[2006,3,14]],"date-time":"2006-03-14T17:24:33Z","timestamp":1142357073000},"page":"287-327","source":"Crossref","is-referenced-by-count":54,"title":["Set theory in first-order logic: Clauses for G\u00f6del's axioms"],"prefix":"10.1007","volume":"2","author":[{"given":"Robert","family":"Boyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ewing","family":"Lusk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"William","family":"McCune","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ross","family":"Overbeek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark","family":"Stickel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lawrence","family":"Wos","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"BF02328452_CR1","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1016\/0004-3702(71)90004-X","volume":"2","author":"W. W. Bledsoe","year":"1971","unstructured":"BledsoeW. W., \u2018Splitting and reduction heuristics in automatic theorem proving\u2019,Artificial Intelligence 2 55\u201377 (1971).","journal-title":"Artificial Intelligence"},{"key":"BF02328452_CR2","doi-asserted-by":"crossref","unstructured":"Bledsoe, W. W., \u2018Some automatic proofs in analysis\u2019, inAutomated Theorem Proving: After 25 Years, (eds. D. Loveland and W. W. Bledsoe), American Mathematical Society (1984).","DOI":"10.1090\/conm\/029"},{"key":"BF02328452_CR3","unstructured":"G\u00f6del, K.,The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Princeton University Press (1940)."},{"key":"BF02328452_CR4","volume-title":"General Topology","author":"J. Kelly","year":"1955","unstructured":"KellyJ.,General Topology, D. van Nostrand, Princeton, New Jersey (1955)."},{"key":"BF02328452_CR5","unstructured":"McDonald, J. and Suppes, P., \u2018Student use of an interactive theorem prover\u2019, inAutomated Theorem Proving: After 25 Years, (eds. D. Loveland and W. W. Bledsoe), American Mathematical Society (1984)."},{"key":"BF02328452_CR6","volume-title":"A Theory of Sets","author":"A. P. Morse","year":"1965","unstructured":"MorseA. P.,A Theory of Sets, Academic Press, New York (1965)."},{"key":"BF02328452_CR7","unstructured":"Pastre, D., \u2018Demonstration automatique de theoremes en theorie des ensembles\u2019, Paris 6 (1976). (Ph.D. thesis)"},{"key":"BF02328452_CR8","unstructured":"Quine, W.,Set Theory and Its Logic, Harvard University Press (1969)."},{"key":"BF02328452_CR9","volume-title":"Mathematical Logic","author":"J. R. Shoenfield","year":"1967","unstructured":"ShoenfieldJ. R.,Mathematical Logic, Addison-Wesley, Reading, Ma. (1967)."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02328452.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF02328452\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF02328452","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T18:07:36Z","timestamp":1558030056000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF02328452"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1986,9]]},"references-count":9,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1986,9]]}},"alternative-id":["BF02328452"],"URL":"https:\/\/doi.org\/10.1007\/bf02328452","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1986,9]]}}}