Класс Бернейса – Шенфинкеля - Bernays–Schönfinkel class

В Класс Бернейса – Шенфинкеля (также известен как Класс Бернейса – Шенфинкеля – Рамсея) формул, названных в честь Пол Бернейс, Моисей Шёнфинкель и Фрэнк П. Рэмси, является фрагментом логика первого порядка формулы, где выполнимость является разрешимый.

Это набор предложений, которые при написании пренекс нормальная форма, есть ${displaystyle exists ^{*}forall ^{*}}$ префикс квантификатора и не содержат функциональные символы.

Этот класс логических формул также иногда называют эффективно пропозициональный (EPR), поскольку его можно эффективно перевести на логика высказываний формулы путем заземления или создания экземпляра.

Проблема выполнимости для этого класса: NEXPTIME -полный.^[1]

Смотрите также

• Prenex нормальная форма

Примечания

1. Льюис, Гарри Р. (1980), "Результаты о сложности классов квантификационных формул", Журнал компьютерных и системных наук, 21 (3): 317–353, Дои:10.1016/0022-0000(80)90027-6, МИСТЕР  0603587

Рекомендации

• Рэмси, Ф. (1930), «О проблеме формальной логики», Proc. Лондонская математика. Soc., 30: 264–286, Дои:10.1112 / плмс / с2-30.1.264
• Piskac, R .; de Moura, L .; Бьорнер, Н. (декабрь 2008 г.), «Эффективное решение пропозициональной логики с равенством» (PDF), Технический отчет Microsoft Research (2008–181)