Bernays–Schönfinkel class: Difference between revisions
Content deleted Content added
m Please avoid cosmetic edits |
Magioladitis (talk | contribs) m v1.41b - WP:WCW project (Link equal to linktext) |
||
| Line 1: | Line 1: | ||
The '''Bernays–Schönfinkel class''' (also known as '''Bernays–Schönfinkel-Ramsey class''') of formulas, named after [[Paul Bernays]] and [[Moses Schönfinkel]] (and [[Frank P. Ramsey]]), is a fragment of [[first-order logic]] formulas where [[ |
The '''Bernays–Schönfinkel class''' (also known as '''Bernays–Schönfinkel-Ramsey class''') of formulas, named after [[Paul Bernays]] and [[Moses Schönfinkel]] (and [[Frank P. Ramsey]]), is a fragment of [[first-order logic]] formulas where [[satisfiability]] is [[Decidability (logic)|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. |
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. |
||
Revision as of 11:10, 27 February 2017
The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel-Ramsey class) of formulas, named after Paul Bernays and 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 quantifier prefix and do not contain any function symbols.
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.[1]
See also
References
- ^ Harry R. Lewis, Complexity Results for Classes of Quantificational Formulas, J. Computer and System Sciences, 21, 317-353 (1980) doi:10.1016/0022-0000(80)90027-6
- 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)
 | This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. |