{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T00:10:28Z","timestamp":1760141428853,"version":"build-2065373602"},"reference-count":32,"publisher":"Elsevier BV","issue":"1","license":[{"start":{"date-parts":[[1988,8,1]],"date-time":"1988-08-01T00:00:00Z","timestamp":586396800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[1988,8,1]],"date-time":"1988-08-01T00:00:00Z","timestamp":586396800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2009,5,28]],"date-time":"2009-05-28T00:00:00Z","timestamp":1243468800000},"content-version":"vor","delay-in-days":7605,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Journal of Symbolic Computation"],"published-print":{"date-parts":[[1988,8]]},"DOI":"10.1016\/s0747-7171(88)80023-3","type":"journal-article","created":{"date-parts":[[2008,5,29]],"date-time":"2008-05-29T06:22:56Z","timestamp":1212042176000},"page":"83-98","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":8,"title":["The automation of syllogistic I. Syllogistic normal forms"],"prefix":"10.1016","volume":"6","author":[{"given":"Domenico","family":"Cantone","sequence":"first","affiliation":[]},{"given":"Susanna","family":"Ghelfo","sequence":"additional","affiliation":[]},{"given":"Eugenio","family":"Omodeo","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0747-7171(88)80023-3_bib1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.2307\/2269097","article-title":"On simplifying truth-functional formulas","volume":"21","author":"Bing","year":"1956","journal-title":"J. Symb. Logic"},{"key":"10.1016\/S0747-7171(88)80023-3_bib2","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1002\/cpa.3160340203","article-title":"Decision procedures for elementary sublanguages of Set Theory. II. Formulas involving restricted quantifiers, together with ordinal, integer, map, and domain notions","volume":"34","author":"Breban","year":"1981","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib3","doi-asserted-by":"crossref","DOI":"10.1016\/0196-8858(84)90007-1","article-title":"Decision procedures for elementary sublanguages of Set Theory. III. Restricted classes of formulas involving the powerset operator and the general set union operator","volume":"5","author":"Breban","year":"1984","journal-title":"Adv. Appl. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib4","doi-asserted-by":"crossref","first-page":"549","DOI":"10.1002\/cpa.3160380507","article-title":"Decision procedures for elementary sublanguages of Set Theory. VI. Multi-level syllogistic extended by the powerset operator","volume":"38","author":"Cantone","year":"1985","journal-title":"Comm. Pure App. Math., Spec. Annivers. Iss."},{"key":"10.1016\/S0747-7171(88)80023-3_bib5","article-title":"Some recent decidability results in set theory","author":"Cantone","year":"1986","journal-title":"X Incontro di Logica Matematica\u2014La Logica nell* Informatica, Siena"},{"key":"10.1016\/S0747-7171(88)80023-3_bib6","series-title":"PhD thesis","article-title":"A decision procedure for a class of unquantified formulae of set theory involving the powerset and singleton operators","author":"Cantone","year":"1987"},{"key":"10.1016\/S0747-7171(88)80023-3_bib7","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1002\/cpa.3160400103","article-title":"Decision procedures for elementary sublanguages of Set Theory. IV. Formulae involving a rank operator or one occurrence of \u03a3(x) = {{y}|y\u2208x}","volume":"40","author":"Cantone","year":"1987","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0022-0000(87)90001-8","article-title":"Decision procedures for elementary sublanguages of Set Theory. V. Multi-level syllogistic extended by the general union operator","volume":"34","author":"Cantone","year":"1987","journal-title":"J. Comp. Syst. Sci."},{"key":"10.1016\/S0747-7171(88)80023-3_bib9","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1002\/cpa.3160400303","article-title":"Decision algorithms for some fragments of analysis and related areas","volume":"40","author":"Cantone","year":"1987","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib10","doi-asserted-by":"crossref","first-page":"105","DOI":"10.1002\/cpa.3160410107","article-title":"Decision procedures for elementary sublanguages of Set Theory. VIII. A semidecision procedure for finite satisfiability of unquantified set-theoretic formulae","volume":"41","author":"Cantone","year":"1988","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib11","first-page":"130","article-title":"An efficient validity test for formulae in extensional two-level syllogistic","volume":"33","author":"Ferro","year":"1978","journal-title":"Le Matematiche (Catania, Italy)"},{"key":"10.1016\/S0747-7171(88)80023-3_bib12","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1002\/cpa.3160330503","article-title":"Decision procedures for elementary sublanguages of Set Theory. I. Multi-level syllogistic and some extensions","volume":"33","author":"Ferro","year":"1980","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib13","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/3-540-10009-1_8","article-title":"Decision procedures for some fragments of Set Theory. Proc. 5th Conf. Automated Deduction","volume":"87","author":"Ferro","year":"1980","journal-title":"Springer Lect. Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(88)80023-3_bib14","doi-asserted-by":"crossref","first-page":"367","DOI":"10.1002\/cpa.3160380403","article-title":"A note on the decidability of MLS extended by the powerset operator","volume":"38","author":"Ferro","year":"1985","journal-title":"Comm. Pure App, Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib15","doi-asserted-by":"crossref","first-page":"265","DOI":"10.1002\/cpa.3160400302","article-title":"Decision procedures for elementary sublanguages of Set Theory. VII. Validity in set theory when a choice operator is present","volume":"40","author":"Ferro","year":"1987","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib16","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1147\/rd.12.0171","article-title":"Irredundant disjunctive and conjunctive forms of a Boolean function","volume":"1","author":"Ghazala","year":"1957","journal-title":"IBM Jl Res. Develop."},{"key":"10.1016\/S0747-7171(88)80023-3_bib17","first-page":"40","article-title":"Towards practical implementations of syllogistic","volume":"204","author":"Ghelfo","year":"1985","journal-title":"Eurocal '85, Proc. Vol. 2. Springer Lect. Notes Comp. Sei."},{"key":"10.1016\/S0747-7171(88)80023-3_bib18","doi-asserted-by":"crossref","DOI":"10.1002\/malq.19780241902","article-title":"The \u2200n \u220b-completeness of Zermelo-Fraenkel Set Theory","author":"Gogol","year":"1978","journal-title":"Zeitschr. f. math. Logik und Grundlagen d. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib19_1","article-title":"Sentences with three quantifiers are decidable in Set Theory","volume":"CII","author":"Gogol","year":"1979","journal-title":"Fundamenta Mathematicae"},{"year":"1978","series-title":"Set Theory","author":"Jech","key":"10.1016\/S0747-7171(88)80023-3_bib19_2"},{"key":"10.1016\/S0747-7171(88)80023-3_bib20","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-10009-1_9","article-title":"Simplifying interpreted formulas. Proc. 5th Conf. Automated Deduction","volume":"87","author":"Loveland","year":"1980","journal-title":"Springer Lect. Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(88)80023-3_bib21","doi-asserted-by":"crossref","first-page":"232","DOI":"10.2307\/2268219","article-title":"Weak simplest normal truth functions","volume":"20","author":"Nelson","year":"1955","journal-title":"J. Symb. Logic"},{"key":"10.1016\/S0747-7171(88)80023-3_bib22","series-title":"PhD thesis","article-title":"Decidability and Proof Procedures for Set Theory with a Choice Operator","author":"Omodeo","year":"1984"},{"key":"10.1016\/S0747-7171(88)80023-3_bib23","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/3-540-19129-1_10","article-title":"Hints for the design of a set calculus oriented to Automated Deduction. Proc. workshop Foundations of Functional and Logic Programming, Trento, 1986","volume":"306","author":"Omodeo","year":"1988","journal-title":"Springer Lect. Notes Comp. Sci."},{"key":"10.1016\/S0747-7171(88)80023-3_bib24","doi-asserted-by":"crossref","first-page":"221","DOI":"10.1002\/cpa.3160410206","article-title":"Decision procedures for elementary sublanguages of Set Theory. IX. Undecidability of set theoretic formulas involving restricted quantifiers","volume":"41","author":"Parlamente","year":"1988","journal-title":"Comm. Pure App. Math."},{"key":"10.1016\/S0747-7171(88)80023-3_bib25","article-title":"Completeness and decidability of the deducibility problem for some class of formulas of set theory","author":"Polcriti","year":"1988","journal-title":"Le Matematiche (Catania, Italy)"},{"key":"10.1016\/S0747-7171(88)80023-3_bib26","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1080\/00029890.1952.11988183","article-title":"The problem of simplifying truth functions","volume":"59","author":"Quine","year":"1952","journal-title":"Amer. Math. Monthly"},{"key":"10.1016\/S0747-7171(88)80023-3_bib27","series-title":"Inst, for Computer Applications in Science and Engr","article-title":"Instantiation and decision procedures for certain classes of quantified set-theoretic formulae","author":"Schwartz","year":"1978"},{"year":"1986","series-title":"Programming with Sets","author":"Schwartz","key":"10.1016\/S0747-7171(88)80023-3_bib28"},{"year":"1964","series-title":"Boolean Algebras","author":"Sikorski","key":"10.1016\/S0747-7171(88)80023-3_bib29"},{"year":"1934","series-title":"Symbolic Logic","author":"Venn","key":"10.1016\/S0747-7171(88)80023-3_bib30"},{"key":"10.1016\/S0747-7171(88)80023-3_bib31","first-page":"513","article-title":"D\u00e9cidabilit\u00e9 des formules existentielles en th\u00e9orie des ensembles","volume":"272","author":"Ville","year":"1971","journal-title":"C.R. Acad. Sci., Paris, Ser. A"}],"container-title":["Journal of Symbolic Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717188800233?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0747717188800233?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T01:18:10Z","timestamp":1760059090000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0747717188800233"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1988,8]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1988,8]]}},"alternative-id":["S0747717188800233"],"URL":"https:\/\/doi.org\/10.1016\/s0747-7171(88)80023-3","relation":{},"ISSN":["0747-7171"],"issn-type":[{"type":"print","value":"0747-7171"}],"subject":[],"published":{"date-parts":[[1988,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"The automation of syllogistic I. Syllogistic normal forms","name":"articletitle","label":"Article Title"},{"value":"Journal of Symbolic Computation","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0747-7171(88)80023-3","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 1988 Published by Elsevier Ltd.","name":"copyright","label":"Copyright"}]}}