Satisfiability of formulae with one \(\forall\) is decidable in exponential time (Q915716)

By predicate logic (with or without equality) the author means first order logic without function symbols. With function symbols present, the author speaks of full first order logic (with or without equality). A prefix class K of formulas is called maximal solvable if it is solvable (i.e. satisfiability for formulas in the class is decidable) and if every prefix class which properly extends K is unsolvable. As set forth by the author, the satisfiability problems for the four maximal solvable classes in predicate logic (without equality, \([\exists^*\forall^ 2\exists^*]\) and \([\exists^*\forall^*]\); with equality, \([\exists^*\forall \exists^*]\) and \([\exists^*\forall^*])\) are NEXPTIME-complete. The author proves that in full first order logic without equality the satisfiability problem for the unique maximal solvable prefix class \([\exists^*\forall \exists^*]\) is dedicable in deterministic exponential time (EXPTIME). In another paper he shows that in full first order logic with equality the satisfiability problem for the unique maximal solvable class \([\exists^*]\) is NP-complete.