Classe Bernays – Schönfinkel - Bernays–Schönfinkel class
A classe Bernays – Schönfinkel (também conhecida como classe Bernays – Schönfinkel – Ramsey ) de fórmulas, nomeada em homenagem a Paul Bernays , Moses Schönfinkel e Frank P. Ramsey , é um fragmento de fórmulas lógicas de primeira ordem onde a satisfatibilidade é decidível .
É o conjunto de sentenças que, quando escritas na forma normal prenex , possuem um prefixo quantificador e não contêm nenhum símbolo de função .
Esta classe de fórmulas lógicas também é algumas vezes referida como efetivamente proposicional ( EPR ), uma vez que pode ser efetivamente traduzida em fórmulas lógicas proposicionais por um processo de fundamentação ou instanciação.
O problema de satisfatibilidade para esta classe é NEXPTIME -complete.
Veja também
Notas
Referências
- Ramsey, F. (1930), "On a problem in formal logic", Proc. London Math. Soc. , 30 : 264-286, doi : 10.1112 / plms / s2-30.1.264
- Piskac, R .; de Moura, L .; Bjorner, N. (dezembro de 2008), "Deciding Effectively Propositional Logic with Equality" (PDF) , Microsoft Research Technical Report (2008–181)