The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after Paul Bernays, Moses Schönfinkel and Frank P. Ramsey, is a fragment of first-order logic formulas where satisfiabilityisdecidable.
It is the set of sentences that, when written in prenex normal form, have an 
Ramsey proved that, if 
This class of logic formulas is also sometimes referred as effectively propositional (EPR) 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.[2]
Efficient algorithms for deciding satisfiability of EPR have been integrated into SMT solvers.[3]
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |