Article collection "Mathematical Problems of Cybernetics" №1, Moscow, 1988
On the complexity of decision problem for some classes of predicate formulas
We consider classes A,B of sentences in the restricted predicate calculus (without equality). The class A consists of all sentences that contain only valence one predicate symbols and have the quantifier prefix ∀∃∃ in their prenex normal form; class B sentences have a quantifier prefix ∀x∃y1∃y2∀z, contain only valence two predicate symbols and contain no atomic formulas matching P(z,x), P(z,y1), P(z,y2). Denote by Sat(A) (respectively Sat(B)) the set of all satisfiable sentences in the class A (class B), and by DT(T(n)) - the class of sets that can be decided by a single tape deterministic Turing machine in T(n) steps. We prove that for appropriately chosen constants a>b>1 holds
Sat(A) ∈ DT(an/logn)\DT(bn/logn),
Sat(A) ∈ DT(aan/logn)\DT(bbn/logn).
complexity of decision problem, restricted predicate calculus