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^[1]^,^[2]. Elle est nommée d'après ses créateurs, Paul Bernays et Moses Schönfinkel (avec l'apport aussi de Frank Ramsey).

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.

Cet article ne cite pas suffisamment ses sources (octobre 2016).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».

En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?

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

Cette classe de formules s'appelle parfois effectively propositional (EPR)^[4] 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)^[5]^,^[6]. 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^[7].

Notes et références

↑ (de) Bernays, Paul, et Moses Schönfinkel, « Zum entscheidungsproblem der mathematischen logik », Mathematische Annalen, t. 99.1,‎ 1928, p. 342-372
↑ (en-GB) Daniel Kroening et Ofer Strichman, Decision Procedures | SpringerLink (DOI 10.1007/978-3-662-50497-0, lire en ligne), p. 325
↑ Harry R. Lewis, « Complexity results for classes of quantificational formulas », Journal of Computer and System Sciences, vol. 21,‎ 1^er décembre 1980, p. 317–353 (DOI 10.1016/0022-0000(80)90027-6, lire en ligne, consulté le 18 octobre 2016)
↑ « Beyond SAT: What About First-Order Logic? », sur users.cecs.anu.edu.au (consulté le 13 janvier 2018)
↑ « Page du solveur iprover »
↑ « Page de la compétition CASC »
↑ (en) Ruzica Piskac, Leonardo de Moura et Nikolaj Bjørner, « Deciding Effectively Propositional Logic Using DPLL and Substitution Sets », Journal of Automated Reasoning, vol. 44, n^o 4,‎ 1^er avril 2010, p. 401–424 (ISSN 0168-7433 et 1573-0670, DOI 10.1007/s10817-009-9161-6, lire en ligne, consulté le 13 janvier 2018)

Portail des mathématiques

[1] (de) Bernays, Paul, et Moses Schönfinkel, « Zum entscheidungsproblem der mathematischen logik », Mathematische Annalen, t. 99.1,‎ 1928, p. 342-372

[2] (en-GB) Daniel Kroening et Ofer Strichman, Decision Procedures | SpringerLink (DOI 10.1007/978-3-662-50497-0, lire en ligne), p. 325

[3] Harry R. Lewis, « Complexity results for classes of quantificational formulas », Journal of Computer and System Sciences, vol. 21,‎ 1^er décembre 1980, p. 317–353 (DOI 10.1016/0022-0000(80)90027-6, lire en ligne, consulté le 18 octobre 2016)

[4] « Beyond SAT: What About First-Order Logic? », sur users.cecs.anu.edu.au (consulté le 13 janvier 2018)

[5] « Page du solveur iprover »

[6] « Page de la compétition CASC »

[7] (en) Ruzica Piskac, Leonardo de Moura et Nikolaj Bjørner, « Deciding Effectively Propositional Logic Using DPLL and Substitution Sets », Journal of Automated Reasoning, vol. 44, n^o 4,‎ 1^er avril 2010, p. 401–424 (ISSN 0168-7433 et 1573-0670, DOI 10.1007/s10817-009-9161-6, lire en ligne, consulté le 13 janvier 2018)

[1]

[2]

[3]

[4]

[5]

[6]

[7]