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 satisfiability is decidable.

It is the set of sentences that, when written in prenex normal form, have an ∃ ∗ ∀ ∗ {\displaystyle \exists ^{*}\forall ^{*}} quantifier prefix and do not contain any function symbols.

Ramsey proved that, if ϕ {\displaystyle \phi } is a formula in the Bernays–Schönfinkel class with one free variable, then either { x ∈ N : ϕ ( x ) } {\displaystyle \{x\in \mathbb {N} :\phi (x)\}} is finite, or { x ∈ N : ¬ ϕ ( x ) } {\displaystyle \{x\in \mathbb {N} :\neg \phi (x)\}} is finite.

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.

Applications

Efficient algorithms for deciding satisfiability of EPR have been integrated into SMT solvers.

See also

Notes

  • Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc., 30: 264–286, doi:
  • Piskac, R.; de Moura, L.; Bjorner, N. (December 2008), (PDF), Microsoft Research Technical Report (2008–181)