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

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

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

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

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

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

Приложения

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

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

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

Примечания

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.

Ссылки

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