{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,2,7]],"date-time":"2023-02-07T00:31:08Z","timestamp":1675729868287},"reference-count":21,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1978,11,1]],"date-time":"1978-11-01T00:00:00Z","timestamp":278726400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[1978,11]]},"DOI":"10.1016\/s0004-3702(78)80017-4","type":"journal-article","created":{"date-parts":[[2006,7,12]],"date-time":"2006-07-12T09:34:30Z","timestamp":1152696870000},"page":"281-316","source":"Crossref","is-referenced-by-count":23,"title":["Towards the automation of set theory and its logic"],"prefix":"10.1016","volume":"10","author":[{"given":"Frank Malloy","family":"Brown","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S0004-3702(78)80017-4_bib1","unstructured":"Quine, W. V. O., Set Theory and its Logic, revised edition 1969, Oxford University Press, London, Library of Congress Catalogue Card No. 68-14271."},{"key":"10.1016\/S0004-3702(78)80017-4_bib2","unstructured":"Brown, F. M., Doing arithmetic without diagrams, DAI Research Report No. 16a, To appear in Artificial Intelligence."},{"key":"10.1016\/S0004-3702(78)80017-4_bib3","author":"Morse","year":"1965"},{"issue":"1","key":"10.1016\/S0004-3702(78)80017-4_bib4","doi-asserted-by":"crossref","DOI":"10.1016\/0004-3702(71)90004-X","article-title":"Splitting and reduction heuristics in automatic theorem proving","volume":"2","author":"Bledsoe","year":"1971","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(78)80017-4_bib5","doi-asserted-by":"crossref","DOI":"10.1016\/0004-3702(72)90041-0","article-title":"Computer proofs of limit theorems","volume":"3","author":"Bledsoe","year":"1972","journal-title":"Artificial Intelligence"},{"key":"10.1016\/S0004-3702(78)80017-4_bib6","article-title":"Proving Theorems about LISP functions","author":"Boyer","year":"1973"},{"key":"10.1016\/S0004-3702(78)80017-4_bib7","unstructured":"Strother Moore, J., Computational logic: Structure sharing and proof of program properties, part II, DCL Memo No. 68."},{"key":"10.1016\/S0004-3702(78)80017-4_bib8","article-title":"Mechanizing structural induction","author":"Aubin","year":"1976"},{"key":"10.1016\/S0004-3702(78)80017-4_bib9","author":"McCarthy","year":"1965"},{"key":"10.1016\/S0004-3702(78)80017-4_bib10","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1147\/rd.41.0002","article-title":"Toward mechanical mathematics","volume":"4","author":"Wang","year":"1960","journal-title":"IBM Journal of Research and Development"},{"key":"10.1016\/S0004-3702(78)80017-4_bib11","doi-asserted-by":"crossref","first-page":"102","DOI":"10.1111\/j.1755-2567.1960.tb00558.x","article-title":"An improved proof procedure","volume":"26","author":"Prawitz","year":"1960","journal-title":"Theoria"},{"key":"10.1016\/S0004-3702(78)80017-4_bib12","first-page":"23","article-title":"A machine-oriented logic based on the resolution principle","volume":"12","author":"Robinson","year":"1965","journal-title":"J.A.C.M."},{"key":"10.1016\/S0004-3702(78)80017-4_bib13","series-title":"International Computing Symposium","article-title":"Proof search in a Gentzen-like system of first order logic","author":"Bibel","year":"1975"},{"key":"10.1016\/S0004-3702(78)80017-4_bib14","article-title":"A modification of the unification algorithm in automatic theorem proving","author":"Siekmann","year":"1972"},{"key":"10.1016\/S0004-3702(78)80017-4_bib15","article-title":"Building in equational theories","volume":"7","author":"Plotkin","year":"1972","journal-title":"Machine Intelligence"},{"key":"10.1016\/S0004-3702(78)80017-4_bib16","article-title":"Canonical algebraic simplification","author":"Lankford","year":"1975"},{"key":"10.1016\/S0004-3702(78)80017-4_bib17","article-title":"A Logic of Action","volume":"6","author":"Hayes","year":"1971","journal-title":"Machine Intelligence"},{"key":"10.1016\/S0004-3702(78)80017-4_bib18","unstructured":"Quam, Lynn, Stanford AT LISP 1.6 Manual, Stanford Artificial Intelligence Laboratory Operating Note 26.6."},{"key":"10.1016\/S0004-3702(78)80017-4_bib19","unstructured":"Bebrow, R. et al., UCI LISP Manual, Technical Report 21, Department of Information and Computer Science, University of California, Irvine."},{"key":"10.1016\/S0004-3702(78)80017-4_bib20","article-title":"Demonstration Automatique de Theoremes en Theorie des Ensembles","author":"Pastre","year":"1976","journal-title":"These de de 3eme cycle"},{"key":"10.1016\/S0004-3702(78)80017-4_bib21","series-title":"Automatic theorem proving in set theory","author":"Pastre","year":"1977"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370278800174?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370278800174?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T22:57:12Z","timestamp":1547506632000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370278800174"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1978,11]]},"references-count":21,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1978,11]]}},"alternative-id":["S0004370278800174"],"URL":"https:\/\/doi.org\/10.1016\/s0004-3702(78)80017-4","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[1978,11]]}}}