{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,31]],"date-time":"2026-01-31T11:42:13Z","timestamp":1769859733595,"version":"3.49.0"},"reference-count":9,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[1990,6,1]],"date-time":"1990-06-01T00:00:00Z","timestamp":644198400000},"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":[[1990,6]]},"DOI":"10.1007\/bf00245817","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T05:54:20Z","timestamp":1096437260000},"page":"173-187","source":"Crossref","is-referenced-by-count":26,"title":["The automation of syllogistic"],"prefix":"10.1007","volume":"6","author":[{"given":"D.","family":"Cantone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"E. G.","family":"Omodeo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"A.","family":"Policriti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"CR1","volume-title":"Data Structures and Algorithms","author":"A. V. Aho","year":"1983","unstructured":"Aho, A. V., Hopcroft, J. E., and Ullman, J. D., Data Structures and Algorithms, Addison-Wesley, Reading, Mass. (1983)."},{"key":"CR2","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1002\/cpa.3160340203","volume":"34","author":"M. Breban","year":"1981","unstructured":"Breban, M., Ferro, A., Omodeo, E. G., and Schwartz, J. T., ?Decision procedures for elementary sublanguages of set theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions?, Comm. Pure App. Math. 34, 177?195 (1981).","journal-title":"Comm. Pure App. Math."},{"key":"CR3","unstructured":"Cantone, D., ?A decision procedure for a class of unquantified formulae of set theory involving the powerset and singleton operators?, PhD Thesis, New York Univ.-GSAS, Courant Institute of Mathematical Sciences, New York (1987)."},{"issue":"1","key":"CR4","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/S0747-7171(88)80023-3","volume":"61","author":"D. Cantone","year":"1988","unstructured":"Cantone, D., Ghelfo, S., and Omodeo, E. G., ?The automation of syllogistic. I. Syllogistic normal forms?, J. Symbol. Comp. 61(1); 83?98 (1988).","journal-title":"J. Symbol. Comp."},{"key":"CR5","doi-asserted-by":"crossref","unstructured":"Ghelfo, S. and Omodeo, E. G., ?Towards practical implementations of syllogistic?, in EUROCAL '85, European Conf. on Computer Algebra-Proceedings, Vol. 2, pp. 40?48, Springer-Verlag (1985).","DOI":"10.1007\/3-540-15984-3_237"},{"key":"CR6","volume-title":"Introduction to Mathematical Logic","author":"E. Mendelson","year":"1964","unstructured":"Mendelson, E., Introduction to Mathematical Logic, Van Nostrand-Reinhold, Princeton, New Jersey (1964)."},{"key":"CR7","unstructured":"Omodeo, E. G., ?Decidability and proof procedures for set theory with a choice operator?, PhD Thesis, New York Univ.-GSAS, Courant Institute of Mathematical Sciences, New York (1984)."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"Parlamento F. and Policriti A., ?The logically simplest form of the infinity axiom; Proc. AMS 103 (1), (May 1988).","DOI":"10.1090\/S0002-9939-1988-0938682-2"},{"key":"CR9","unstructured":"Parlamento, F. and Policriti, A., ?Decision procedures for elementary sublanguages of set theory. XIII. Model graphs, reflection and decidability?, J. Symb. Comp., ? Special issue (to appear). New Trends in Automated Mathematical Reasoning-Proceedings."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245817.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00245817\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00245817","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T06:58:08Z","timestamp":1585897088000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00245817"}},"subtitle":["II. Optimization and complexity issues"],"short-title":[],"issued":{"date-parts":[[1990,6]]},"references-count":9,"journal-issue":{"issue":"2","published-print":{"date-parts":[[1990,6]]}},"alternative-id":["BF00245817"],"URL":"https:\/\/doi.org\/10.1007\/bf00245817","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[1990,6]]}}}