|
The Bernays–Schönfinkel class of formulas, named after Paul Bernays and Moses Schönfinkel, is a decidable fragment of first-order logic formulas. It corresponds to formulas which, when written in prenex normal form, have an quantifier prefix and do not contain any function symbols. This class of formulas are also sometimes known as effectively propositional (EPR) since they can be effectively translated into propositional logic formulas by a process of grounding or instantiation.
| ||||||||
|
| |||||||||
 |
|
| |