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 [math]\displaystyle{ \exists^*\forall^* }[/math] quantifier prefix and do not contain any function symbols.

Ramsey proved that, if [math]\displaystyle{ \phi }[/math] is a formula in the Bernays–Schönfinkel class with one free variable, then either [math]\displaystyle{ \\{x \in \N : \phi(x)\\} }[/math] is finite, or [math]\displaystyle{ \\{x \in \N : \neg \phi(x)\\} }[/math] 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]

## Contents

* 1 Applications
* 2 See also
* 3 Notes
* 4 References

## 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) (in en). Fragments of First-Order Logic. Oxford University Press. pp. 186. ISBN 978-0-19-196006-2. https://academic.oup.com/book/46400.
2. ↑ "Complexity results for classes of quantificational formulas", Journal of Computer and System Sciences 21 (3): 317–353, 1980, doi:10.1016/0022-0000(80)90027-6
3. ↑ de Moura, Leonardo; Bjørner, Nikolaj (2008). Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles. eds. "Deciding Effectively Propositional Logic Using DPLL and Substitution Sets" (in en). 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. https://link.springer.com/chapter/10.1007/978-3-540-71070-7_35.

## 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", Microsoft Research Technical Report (2008-181), https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2008-181.pdf

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Bernays–Schönfinkel class. Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Philosophy:Bernays–Schönfinkel_class&oldid=3288959"