Classe de Bernays-Schönfinkel
# Classe de Bernays-Schönfinkel

En logique mathématique, la classe de Bernays-Schönfinkel (parfois appelée la classe de Bernays-Schönfinkel-Ramsey) est le fragment syntaxique de la logique du premier ordre des formules dont la forme prénexe est de la forme $\exists ^{*}\forall ^{*}$et qui ne contiennent pas de symboles de $fonctions^,.$ Elle est nommée d'après ses créateurs, Paul Bernays et Moses Schönfinkel (avec l'apport aussi de Frank Ramsey).

Le problème de la satisfiabilité est décidable et NEXPTIME-complet.

Cette classe de formules s'appelle parfois effectively propositional (EPR) car elle peut être effectivement traduite en logique propositionnelle en instanciant les variables universelles par des termes clos.

## Solveurs

La classe de Bernays-Schönfinkel fait l'objet d'une catégorie (elle s'appelle alors EPR) dans la compétition CASC (pour CADE ATP System Competition, où CADE est la conférence Conference on Automated Deduction et ATP signifie Automated theorem $proving)^,.$ Une pratique possible pour résoudre EPR en pratique est d'utiliser les techniques comme DPLL pour le problème SAT de la logique propositionnelle tout en gardant la concision d'EPR.

