HOME

TheInfoList



OR:

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 \exists^*\forall^* 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 \phi 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