On minimizing the \(\forall\)-\(\neg\) degree of a connective-free formula (Q1323356)

The class of connective-free formulas (i.e., the predicate formulas built using only quantifiers and negation) is studied. The algorithmic problem of finding, for a given formula, all classically equivalent formulas with the minimal number of negations and universal quantifiers is solved (this form of minimization arises from some investigations of nested relational databases). The number of such minimal formulas is in general exponential. On the other hand, the associated decision, search and enumeration problems are solved in polynomial time.