Bernays–Schönfinkel class

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 ${\displaystyle \{x\in \mathbb {N} :\phi (x)\}}$ is finite, or ${\displaystyle \{x\in \mathbb {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.[2]

Applications

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

See also

• Prenex normal form

Notes

1. Pratt-Hartmann, Ian (2023-03-30). Fragments of First-Order Logic. Oxford University Press. p. 186. ISBN 978-0-19-196006-2.
2. Lewis, Harry R. (1980), "Complexity results for classes of quantificational formulas", Journal of Computer and System Sciences, 21 (3): 317–353, doi:10.1016/0022-0000(80)90027-6, MR 0603587
3. de Moura, Leonardo; Bjørner, Nikolaj (2008). Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (eds.). "Deciding Effectively Propositional Logic Using DPLL and Substitution Sets". Automated Reasoning. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer: 410–425. doi:10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.

References

• Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc., 30: 264–286, doi:10.1112/plms/s2-30.1.264
• Piskac, R.; de Moura, L.; Bjorner, N. (December 2008), "Deciding Effectively Propositional Logic with Equality" (PDF), Microsoft Research Technical Report (2008–181)