From Wikipedia, the free encyclopedia
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
{
x
∈
N
:
ϕ
(
x
)
}
{\displaystyle \{x\in \mathbb {N} :\phi (x)\}}
is finite, or
{
x
∈
N
:
¬
ϕ
(
x
)
}
{\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
Notes
^ Pratt-Hartmann, Ian (2023-03-30).
Fragments of First-Order Logic . Oxford University Press. p. 186.
ISBN
978-0-19-196006-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
^ 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)