Bernays-Schönfinkel třída
V matematické logice je třída Bernays-Schönfinkel (někdy nazývaná třída Bernays-Schönfinkel-Ramsey ) syntaktickým fragmentem logiky prvního řádu vzorců, jejichž forma dodatku je forma a která neobsahují symboly funkcí. Je pojmenována podle svých tvůrců, Paula Bernayse a Mosese Schönfinkela (rovněž s příspěvky Franka Ramseyho ).
∃∗∀∗{\ displaystyle \ existuje ^ {*} \ pro všechny ^ {*}}
Problém uspokojivosti je rozhodnutelný a NEXPTIME -kompletní.
Tato třída vzorců se někdy nazývá efektivně propoziční ( EPR ), protože ji lze efektivně převést do propoziční logiky vytvořením instance univerzálních proměnných s uzavřenými termíny.
Řešitelé
Třída Bernays-Schönfinkel je předmětem kategorie (později se jí říká EPR) v soutěži CASC (pro CADE ATP System Competition, kde CADE je konference o automatizovaném odečtu a ATP je zkratka pro Automated theorem proving). Jednou z možných praktik řešení EPR v praxi je použití technik jako DPLL pro SAT problém výrokové logiky při zachování EPR stručně.
Poznámky a odkazy
-
(De) Bernays, Paul a Moses Schönfinkel, „ Zum entscheidungsproblem der mathematischen logik “ , Mathematische Annalen , t. 99,1,1928, str. 342-372
-
(en-GB) Daniel Kroening a Ofer Strichman , rozhodovací postupy | SpringerLink ( DOI 10.1007 / 978-3-662-50497-0 , číst online ) , s. 325
-
Harry R. Lewis , „ Výsledky složitosti pro třídy kvantifikačních vzorců “, Journal of Computer and System Sciences , sv. 21,1 st 12. 1980, str. 317–353 ( DOI 10.1016 / 0022-0000 (80) 90027-6 , číst online , přistupováno 18. října 2016 )
-
„ Beyond SAT: What About First-Order Logic? » , Na users.cecs.anu.edu.au (přístup 13. ledna 2018 )
-
„ Stránka řešitele iproveru “
-
„ Stránka soutěže CASC “
-
(in) Ruzica Piskac , Leonardo Moura a Nikolaj Bjørner , „ Efektivní rozhodování pomocí propoziční logiky DPLL a substitučních sad “ , Journal of Automated Reasoning , sv. 44, n O 4,1 st 04. 2010, str. 401-424 ( ISSN 0168-7433 a 1573-0670 , DOI 10.1007 / s10817-009-9161-6 , číst online , přístup k 13. lednu 2018 )
<img src="https://fr.wikipedia.org/wiki/Special:CentralAutoLogin/start?type=1x1" alt="" title="" width="1" height="1" style="border: none; position: absolute;">