{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,2]],"date-time":"2022-04-02T10:30:00Z","timestamp":1648895400339},"reference-count":15,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":11699,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1982,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A <jats:italic>Krom<\/jats:italic> formula of pure quantification theory is a formula in conjunctive normal form such that each conjunct is a disjunction of at most <jats:italic>two<\/jats:italic> atomic formulas or negations of atomic formulas. Every class of Krom formulas that is determined by the form of their quantifier prefixes and which is known to have an unsolvable decision problem for satisfiability is here shown to be a <jats:italic>conservative<\/jats:italic> reduction class. Therefore both the general satisfiability problem, and the problem of satisfiability in finite models, can be effectively reduced from arbitrary formulas to Krom formulas of these several prefix types.<\/jats:p>","DOI":"10.2307\/2273385","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:58:32Z","timestamp":1146952712000},"page":"110-130","source":"Crossref","is-referenced-by-count":2,"title":["Conservative reduction classes of Krom formulas"],"prefix":"10.1017","volume":"47","author":[{"given":"St\u00e5l O.","family":"Aanderaa","sequence":"first","affiliation":[]},{"given":"Egon","family":"B\u00f6rger","sequence":"additional","affiliation":[]},{"given":"Harry R.","family":"Lewis","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200044741_ref015","first-page":"953","article-title":"O rekursivnoi otdyelimosti","volume":"88","author":"Trakhtenbrot","year":"1953","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200044741_ref014","first-page":"569","article-title":"Nevozmozhnost' algorifma dlya problemy razreshimosti na konechnykh klassakh","volume":"70","author":"Trakhtenbrot","year":"1950","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200044741_ref013","volume-title":"Computation: finite and infinite machines","author":"Minsky","year":"1967"},{"key":"S0022481200044741_ref012","first-page":"17","article-title":"Obratniy metod ystanovleniya vyvodimosti v klassicheskom ischislenii predikatov","volume":"159","author":"Maslov","year":"1964","journal-title":"Doklady Akademii Nauk SSSR"},{"key":"S0022481200044741_ref010","volume-title":"Unsolvable classes of quantificational formulas","author":"Lewis","year":"1979"},{"key":"S0022481200044741_ref008","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19670130104"},{"key":"S0022481200044741_ref007","doi-asserted-by":"publisher","DOI":"10.1007\/BF02007254"},{"key":"S0022481200044741_ref006","volume-title":"The decision problem: Solvable classes of quantificational formulas","author":"Dreben","year":"1979"},{"key":"S0022481200044741_ref002","volume-title":"Archiv f\u00fcr Mathematische Logik und Grundlagenforschung","author":"Aanderaa"},{"key":"S0022481200044741_ref003","first-page":"628","volume":"38","author":"Aanderaa","year":"1973","journal-title":"Prefix classes of Krom formulas"},{"key":"S0022481200044741_ref011","first-page":"471","volume":"38","author":"Lewis","year":"1973","journal-title":"The decision problem for formulas with a small number of atomic subformulas"},{"key":"S0022481200044741_ref009","first-page":"210","volume":"35","author":"Krom","year":"1970","journal-title":"The decision problem for formulas in prenex conjunctive normal form with binary disjunctions"},{"key":"S0022481200044741_ref001","first-page":"1","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"Aanderaa","year":"1971"},{"key":"S0022481200044741_ref005","volume-title":"Reduktionstypen der klassischen Pr\u00e4dikatenlogik","author":"B\u00f6rger","year":"1972"},{"key":"S0022481200044741_ref004","unstructured":"B\u00f6rger E. , Reduktionstypen in Krom- und Hornformeln, Inauguraldissertation, Westf\u00e4lische Wilhelms-Universit\u00e4t, M\u00fcnster, 1971."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200044741","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T21:42:56Z","timestamp":1558734176000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200044741\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1982,3]]},"references-count":15,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1982,3]]}},"alternative-id":["S0022481200044741"],"URL":"https:\/\/doi.org\/10.2307\/2273385","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1982,3]]}}}