Bernays–Schönfinkel class explained

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

\exists ^{*\forall} ^{*} quantifier prefix and do not contain any function symbols.

Ramsey proved that, if

\phi is a formula in the Bernays–Schönfinkel class with one free variable, then either \{x \in \N : \phi(x)\} is finite, or \{x \in \N : \neg \phi(x)\} is finite.^[1]

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.^[2]

See also

• Prenex normal form

Notes and References

1. Book: Pratt-Hartmann, Ian . Fragments of First-Order Logic . 2023-03-30 . Oxford University Press . 978-0-19-196006-2 . 186 . en.
2. de Moura . Leonardo . Bjørner . Nikolaj . 2008 . Armando . Alessandro . Baumgartner . Peter . Dowek . Gilles . Deciding Effectively Propositional Logic Using DPLL and Substitution Sets . Automated Reasoning . Lecture Notes in Computer Science . en . Berlin, Heidelberg . Springer . 410–425 . 10.1007/978-3-540-71070-7_35 . 978-3-540-71070-7.