Klasa Bernaysa-Schönfinkela

Klasa Bernays – Schönfinkel (znana również jako klasa Bernays – Schönfinkel – Ramsey ) formuł, nazwana na cześć Paula Bernaysa , Mosesa Schönfinkela i Franka P. Ramseya , jest fragmentem formuł logicznych pierwszego rzędu , w których spełnialność jest rozstrzygalna .

$kwantyfikatora$ zbiór zdań, które zapisane w mają przedrostek i nie zawierają żadnych symboli funkcyjnych .

Ta klasa formuł logicznych jest czasami określana jako efektywnie zdaniowa ( EPR ), ponieważ można ją skutecznie przetłumaczyć na formuły logiczne zdaniowe w procesie uziemienia lub tworzenia instancji.

Problem spełnialności dla tej klasy jest NEXPTIME -complete.

Zobacz też

• Postać normalna prenexu

Notatki

• Ramsey, F. (1930), „O problemie w logice formalnej”, Proc. Matematyka Londynu. soc. , 30 : 264–286, doi : 10.1112/plms/s2-30.1.264
• Piskac, R.; de Moura, L.; Bjorner, N. (grudzień 2008), „Efektywne podejmowanie decyzji z logiką zdań z równością” (PDF) , Microsoft Research Technical Report (2008–181)