Complexity results for classes of quantificational formulas

摘要

We analyze the computational complexity of determining whether F is satisfiable when F is a formula of the classical predicate calculus obeying certain syntactic restrictions. For example, for the monadic predicate calculus and the Gödel or 3 … ∃∀∀∃ … 3 prefix class we obtain lower and upper nondeterministic time bounds of the form cn/log n. The lower bounds are established by using acceptance problems for time-bounded Turing machines and alternating pushdown and stack automata.