Abstract
Let Kr be the class of all those quantificational formulas whose matrices are conjunctions of binary disjunctions of signed atomic formulas. Decision problems for subclasses of Kr do not invariably coincide with those for the corresponding classes of quantificational formulas with unrestricted matrices; for example, the ∀∃∀ prefix subclass of Kr is solvable, but the full ∀∃∀ class is not ([AaLe],- [KMW]). Moreover, the straightforward encodings of automata which have been used to show the unsolvability of various subclasses of Kr ([Aa], [Bö], [AaLe]) yield but little information about signature subclasses, i.e. subclasses determined by the number and degrees of the predicate letters occurring in a formula. By a new and highly complex construction Theorem 1 establishes the best possible result on classification by signature.Theorem 1. Let C be the class of all formulas in Kr with a single predicate letter, which is dyadic; then C is a reduction class for satisfiability.Thus a signature subclass of Kr is solvable just in case the corresponding class of unrestricted quantificational formulas is solvable, to wit, just in case no predicate letter of degree exceeding one may occur. To obtain a richer classification by signature we consider further restrictions on the matrix. Let Or be the class of formulas in Kr having disjunctive normal forms with only two disjuncts. Theorem 2 sharpens Orevkov's proof of the unsolvability of Or ([Or]; see also [LeGo]).Theorem 2. Let D be the class of formulas in Or with just two predicate letters, both pentadic; then D is a reduction class for satisfiability.