{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,3]],"date-time":"2023-01-03T07:27:29Z","timestamp":1672730849327},"reference-count":14,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":14711,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[1973,12]]},"abstract":"<jats:p>In this paper we consider decision problems for subclasses of <jats:italic>Kr<\/jats:italic>, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of <jats:italic>Q<\/jats:italic><jats:sub>1<\/jats:sub>, \u2026, <jats:italic>Q<jats:sub>n<\/jats:sub><\/jats:italic> is an \u2200 or an \u2203, then let <jats:italic>Q<\/jats:italic><jats:sub>1<\/jats:sub> \u2026 <jats:italic>Q<jats:sub>n<\/jats:sub><\/jats:italic> be the class of those closed prenex formulas with prefixes of the form (<jats:italic>Q<\/jats:italic><jats:sub>1<\/jats:sub><jats:italic>x<\/jats:italic><jats:sub>1<\/jats:sub>)\u2026 (<jats:italic>Q<jats:sub>n<\/jats:sub>x<jats:sub>n<\/jats:sub><\/jats:italic>). Our results may then be stated as follows:<\/jats:p><jats:p>Theorem 1. <jats:italic>The decision problem for satisfiability is solvable for the class<\/jats:italic> \u2200\u2203\u2200 \u2229 <jats:italic>Kr<\/jats:italic>.<\/jats:p><jats:p>Theorem 2. <jats:italic>The classes \u2200\u2203\u2200\u2200 \u2229 Kr and \u2200\u2200\u2203\u2200 \u2229 Kr are reduction classes for satisfiability<\/jats:italic>.<\/jats:p><jats:p>Maslov [11] showed that the class \u2203\u2026\u2203\u2200\u2026\u2200\u2203\u2026\u2203 \u2229 <jats:italic>Kr<\/jats:italic> is solvable, while the first author [1, Corollary 4] showed \u2203\u2200\u2203\u2200 \u2229 <jats:italic>Kr<\/jats:italic> and \u2200\u2203\u2203\u2200 \u2229 <jats:italic>Kr<\/jats:italic> to be reduction classes. Thus the only prefix subclass of <jats:italic>Kr<\/jats:italic> for which the decision problem remains open is \u2200\u2203\u2200\u2203\u2026\u2203\u2229 <jats:italic>Kr<\/jats:italic>.<\/jats:p><jats:p>The class \u2200\u2203\u2200 \u2229 <jats:italic>Kr<\/jats:italic>, though solvable, contains formulas whose only models are infinite (e.g., (\u2200<jats:italic>x<\/jats:italic>)(\u2203<jats:italic>u<\/jats:italic>)(\u2200<jats:italic>y<\/jats:italic>)[(<jats:italic>Pxy<\/jats:italic> \u2228 <jats:italic>Pyx<\/jats:italic>) \u2227 (\u00ac <jats:italic>Pxy<\/jats:italic> \u2228 \u00ac<jats:italic>Pyu<\/jats:italic>)], which can be satisfied over the integers by taking <jats:italic>P<\/jats:italic> to be \u2265). This is not the case for Maslov's class \u2203\u2026\u2203\u2200\u2026\u2200\u2203\u2026\u2203 \u2229 <jats:italic>Kr<\/jats:italic>, which contains no formula whose only models are infinite ([2] [5]).<\/jats:p><jats:p>Theorem 1 was announced in [1, Theorem 4], but the proof sketched there is defective: Lemma 4 (p. 17) is incorrectly stated. Theorem 2 was announced in [9].<\/jats:p>","DOI":"10.2307\/2271987","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T21:26:19Z","timestamp":1146950779000},"page":"628-642","source":"Crossref","is-referenced-by-count":6,"title":["Prefix classes of Krom formulas"],"prefix":"10.1017","volume":"38","author":[{"given":"St\u00e5l O.","family":"Aanderaa","sequence":"first","affiliation":[]},{"given":"Harry R.","family":"Lewis","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200055377_ref014","first-page":"23","volume-title":"Proceedings of a Symposium on the Mathematical Theory of Automata","author":"Wang","year":"1963"},{"key":"S0022481200055377_ref011","first-page":"1420","article-title":"An inverse method of establishing deducibilities in the classical predicate calculus","volume":"5","author":"Maslov","year":"1964","journal-title":"Soviet Mathematics Doklady"},{"key":"S0022481200055377_ref009","first-page":"A","article-title":"Two reduction classes of Krom formulae","volume":"19","author":"Lewis","year":"1972","journal-title":"Notices of the American Mathematical Society"},{"key":"S0022481200055377_ref008","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19670130104"},{"key":"S0022481200055377_ref010","first-page":"471","volume":"38","author":"Lewis","year":"1973","journal-title":"The decision problem for formulas with a small number of atomic subformulas"},{"key":"S0022481200055377_ref007","first-page":"333","article-title":"Bounded ALGOL-like languages","volume":"113","author":"Ginsburg","year":"1964","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0022481200055377_ref005","unstructured":"Dreben B. and Goldfarb W. D. , A systematic treatment of the decision problem (forthcoming)."},{"key":"S0022481200055377_ref004","volume-title":"Introduction to mathematical logic","volume":"I","author":"Church","year":"1956"},{"key":"S0022481200055377_ref012","doi-asserted-by":"publisher","DOI":"10.1145\/321356.321364"},{"key":"S0022481200055377_ref013","first-page":"395","volume-title":"\u00dcber die Vollst\u00e4ndigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt","author":"Presburger","year":"1930"},{"key":"S0022481200055377_ref002","first-page":"A","article-title":"Finite controllability of the Maslov class","volume":"20","author":"Aanderaa","year":"1973","journal-title":"Notices of the American Mathematical Society"},{"key":"S0022481200055377_ref003","volume-title":"Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik","author":"B\u00f6rger"},{"key":"S0022481200055377_ref006","volume-title":"The mathematical theory of context-free languages","author":"Ginsburg","year":"1966"},{"key":"S0022481200055377_ref001","first-page":"1","volume-title":"Proceedings of the Second Scandinavian Logic Symposium","author":"Aanderaa","year":"1971"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200055377","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T19:22:23Z","timestamp":1559244143000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200055377\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1973,12]]},"references-count":14,"journal-issue":{"issue":"4","published-print":{"date-parts":[[1973,12]]}},"alternative-id":["S0022481200055377"],"URL":"https:\/\/doi.org\/10.2307\/2271987","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[1973,12]]}}}