класс Бернейса–Шенфинкеля

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

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

Рэмси доказал, что если — формула класса Бернайса–Шенфинкеля с одной свободной переменной, то либо конечна, либо конечна. ^[1] $\фи$ $\{x\in \mathbb {N} :\phi (x)\}$ $\{x\in \mathbb {N} :\neg \phi (x)\}$

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

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

Приложения

Эффективные алгоритмы для определения выполнимости EPR были интегрированы в решатели SMT . ^[3]

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

Нормальная предварительная форма

Примечания

^ Пратт-Хартманн, Ян (2023-03-30). Фрагменты логики первого порядка. Oxford University Press. стр. 186. ISBN 978-0-19-196006-2.
^ Льюис, Гарри Р. (1980), «Результаты сложности для классов квантификационных формул», Журнал компьютерных и системных наук , 21 (3): 317– 353, doi :10.1016/0022-0000(80)90027-6, MR 0603587
^ де Моура, Леонардо; Бьёрнер, Николай (2008). Армандо, Алессандро; Баумгартнер, Питер; Довек, Жиль (ред.). «Эффективное решение пропозициональной логики с использованием DPLL и наборов подстановок». Автоматизированное рассуждение . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 410– 425. doi :10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.

Ссылки

Рэмси, Ф. (1930), «Об одной проблеме формальной логики», Proc. London Math. Soc. , 30 : 264–286 , doi :10.1112/plms/s2-30.1.264
Пискац, Р.; де Моура, Л.; Бьорнер, Н. (декабрь 2008 г.), «Эффективное решение пропозициональной логики с помощью равенства» (PDF) , Технический отчет Microsoft Research ( 2008–181 )

Эта статья, связанная с математической логикой, является заглушкой . Вы можете помочь Википедии, расширив ее.

[1] Пратт-Хартманн, Ян (2023-03-30). Фрагменты логики первого порядка. Oxford University Press. стр. 186. ISBN 978-0-19-196006-2.

[2] Льюис, Гарри Р. (1980), «Результаты сложности для классов квантификационных формул», Журнал компьютерных и системных наук , 21 (3): 317– 353, doi :10.1016/0022-0000(80)90027-6, MR 0603587

[3] де Моура, Леонардо; Бьёрнер, Николай (2008). Армандо, Алессандро; Баумгартнер, Питер; Довек, Жиль (ред.). «Эффективное решение пропозициональной логики с использованием DPLL и наборов подстановок». Автоматизированное рассуждение . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 410– 425. doi :10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.