This is an old revision of the document!
Classical Decision Problem
Consider satisfiability problem for sentences in first-order logic.
Without loss of generality, assume that formulas are in prenex form.
Classify formulas according to
- regular expression describing the sequence of quantifiers (e.g. means formulas )