Loading AI tools
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 quantifier prefix and do not contain any function symbols.
Ramsey proved that, if is a formula in the Bernays–Schönfinkel class with one free variable, then either is finite, or 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]
Efficient algorithms for deciding satisfiability of EPR have been integrated into SMT solvers.[3]
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.