{{Short description|Concept in first-order logic}} 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 <math>\exists^*\forall^*</math> quantifier prefix and do not contain any function symbols.
Ramsey proved that, if <math>\phi</math> is a formula in the Bernays–Schönfinkel class with one free variable, then either <math>\{x \in \N : \phi(x)\} </math> is finite, or <math>\{x \in \N : \neg \phi(x)\} </math> is finite.<ref>{{Cite book |last=Pratt-Hartmann |first=Ian |url=https://academic.oup.com/book/46400 |title=Fragments of First-Order Logic |date=2023-03-30 |publisher=Oxford University Press |isbn=978-0-19-196006-2 |pages=186 |language=en}}</ref>
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.<ref>{{citation | last = Lewis | first = Harry R. | authorlink = Harry R. Lewis | doi = 10.1016/0022-0000(80)90027-6 | issue = 3 | journal = Journal of Computer and System Sciences | mr = 603587 | pages = 317–353 | title = Complexity results for classes of quantificational formulas | volume = 21 | year = 1980| doi-access = }}</ref>
==Applications==
Efficient algorithms for deciding satisfiability of EPR have been integrated into SMT solvers.<ref>{{Cite book |last1=de Moura |first1=Leonardo |last2=Bjørner |first2=Nikolaj |date=2008 |editor-last=Armando |editor-first=Alessandro |editor2-last=Baumgartner |editor2-first=Peter |editor3-last=Dowek |editor3-first=Gilles |chapter=Deciding Effectively Propositional Logic Using DPLL and Substitution Sets |chapter-url=https://link.springer.com/chapter/10.1007/978-3-540-71070-7_35 |title=Automated Reasoning |series=Lecture Notes in Computer Science |language=en |location=Berlin, Heidelberg |publisher=Springer |pages=410–425 |doi=10.1007/978-3-540-71070-7_35 |isbn=978-3-540-71070-7|chapter-url-access=subscription }}</ref>
==See also== *Prenex normal form
==Notes== {{Reflist}}
==References== *{{Citation | doi=10.1112/plms/s2-30.1.264 | last1=Ramsey | first1=F. | title=On a problem in formal logic |authorlink=Frank P. Ramsey | year=1930 | journal=Proc. London Math. Soc. | volume=30 | pages=264–286 }} *{{Citation | last1=Piskac | first1=R. | last2=de Moura | first2=L. | last3=Bjorner | first3=N. | journal=Microsoft Research Technical Report |date=December 2008 | title=Deciding Effectively Propositional Logic with Equality | issue=2008–181 | url=https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2008-181.pdf }}
{{DEFAULTSORT:Bernays-Schönfinkel class}} Category:Predicate logic
{{mathlogic-stub}}