| Abstrakt: |
In this paper we consider decision problems for subclasses of Kr, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of Q1, …, Qnis an ? or an ?, then let Q1… Qnbe the class of those closed prenex formulas with prefixes of the form (Q1x1)… (Qnxn). Our results may then be stated as follows:Theorem 1. The decision problem for satisfiability is solvable for the class??? n Kr.Theorem 2. The classes ???? n Kr and ???? n Kr are reduction classes for satisfiability.Maslov [11] showed that the class ?…??…??…? n Kris solvable, while the first author [1, Corollary 4] showed ???? n Krand ???? n Krto be reduction classes. Thus the only prefix subclass of Krfor which the decision problem remains open is ????…?n Kr.The class ??? n Kr, though solvable, contains formulas whose only models are infinite (e.g., (?x)(?u)(?y)[(Pxy? Pyx) ? (¬ Pxy? ¬Pyu)], which can be satisfied over the integers by taking Pto be =). This is not the case for Maslov's class ?…??…??…? n Kr, which contains no formula whose only models are infinite ([2] [5]).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]. |
