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

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

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

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

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

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

Приложения

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

См. также

Пренекс нормальная форма

Примечания

^ Пратт-Хартманн, Ян (30 марта 2023 г.). Фрагменты логики первого порядка . Издательство Оксфордского университета. п. 186. ИСБН 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. дои : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7 .

Ссылки

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

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

[1] Пратт-Хартманн, Ян (30 марта 2023 г.). Фрагменты логики первого порядка . Издательство Оксфордского университета. п. 186. ИСБН 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. дои : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7 .

[1]

[2]

[3]