Bernays–Schönfinkel class
The Bernays–Schönfinkel class of formulas, named after Paul Bernays, Moses Schönfinkel and Frank P. Ramsey, is a fragment of first-order logic formulas where satisfiability is decidable.
It is the set of sentences that, when written in prenex normal form, have an quantifier prefix and do not contain any function symbols.
This class of logic formulas is also sometimes referred as effectively propositional since it can be effectively translated into propositional logic formulas by a process of grounding or instantiation.
The satisfiability problem for this class is NEXPTIME-complete.
