Bernays–Schönfinkel (Mathematical Logic)

The Bernays–Schönfinkel is a decidable fragment of first-order logic formulas, in prenex \forsome^* \forall^* (not contain function symbols).

This class of logic is called effectively propositional (EPR) since it can be effectively translated into propositional logic formulas by a process of grounding or instantiation.

References

• https://en.wikipedia.org/wiki/Bernays%E2%80%93Sch%C3%B6nfinkel_class