The Bernays–Schönfinkel class (also known as Bernays–Schönfinkel–Ramsey class) of formulas, named after
Paul Bernays
Paul Isaac Bernays ( ; ; 17 October 1888 – 18 September 1977) was a Swiss mathematician who made significant contributions to mathematical logic, axiomatic set theory, and the philosophy of mathematics. He was an assistant and close collaborator ...
,
Moses Schönfinkel and
Frank P. Ramsey
Frank Plumpton Ramsey (; 22 February 1903 – 19 January 1930) was a British people, British philosopher, mathematician, and economist who made major contributions to all three fields before his death at the age of 26. He was a close friend of ...
, is a fragment of
first-order logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over ...
formulas where
satisfiability
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
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 symbol
In formal logic and related branches of mathematics, a functional predicate, or function symbol, is a logical symbol that may be applied to an object term to produce another object term.
Functional predicates are also sometimes called mappings, bu ...
s.
Ramsey proved that, if
is a formula in the Bernays–Schönfinkel class with one free variable, then either
is finite, or
is finite.
This class of logic formulas is also sometimes referred as effectively propositional (EPR) since it can be effectively translated into
propositional logic
The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...
formulas by a process of grounding or instantiation.
The satisfiability problem for this class is
NEXPTIME
In computational complexity theory, the complexity class NEXPTIME (sometimes called NEXP) is the set of decision problems that can be solved by a non-deterministic Turing machine using time 2^.
In terms of NTIME,
:\mathsf = \bigcup_ \mathsf(2^)
...
-complete.
Applications
Efficient algorithms for deciding satisfiability of EPR have been integrated into
SMT solvers.
See also
*
Prenex normal form
Notes
References
*
*
Predicate logic
{{mathlogic-stub