Логика с двумя переменными

В логике и информатике математической логика двух переменных — это фрагмент логики первого порядка , где формулы можно записать, используя только две разные переменные . ^[1] Этот фрагмент обычно изучается без функциональных символов .

Разрешимость

Некоторые важные проблемы логики двух переменных, такие как выполнимость и конечная выполнимость , разрешимы . ^[2] Этот результат обобщает результаты о разрешимости фрагментов логики двух переменных, таких как некоторые логики описания ; однако некоторые фрагменты логики с двумя переменными имеют гораздо меньшую вычислительную сложность для решения проблем выполнимости.

Напротив, для фрагмента логики первого порядка с тремя переменными без функциональных символов выполнимость неразрешима. ^[3]

Подсчет кванторов

Известно, что двухпеременный фрагмент логики первого порядка без функциональных символов разрешим даже с добавлением кванторов счетных ^[4] и, следовательно, количественной оценки уникальности . Это более мощный результат, поскольку квантификаторы для больших числовых значений не выражаются в этой логике.

Кванторы счета на самом деле улучшают выразительность логики с конечными переменными, поскольку позволяют сказать, что существует узел с $n$ соседи, а именно $\Phi =\exists x\exists ^{\geq n}yE(x,y)$ . Без подсчета кванторов $n+1$ переменные необходимы для одной и той же формулы.

Подключение к алгоритму Вейсфейлера-Лемана

Существует сильная связь между логикой двух переменных и алгоритмом Вейсфейлера-Лемана (или уточнения цвета ). Учитывая два графа, любые два узла имеют одинаковый стабильный цвет при уточнении цвета тогда и только тогда, когда они имеют одинаковый цвет. $C^{2}$ типа, то есть они удовлетворяют одним и тем же формулам в логике двух переменных со счетом. ^[5]

Ссылки

^ Л. Хенкин. Логические системы, содержащие только конечное число символов , Отчет математического факультета Монреальского университета, 1967 г.
^ Э. Гредель, П. Г. Колайтис и М. Варди, О проблеме принятия решения для логики первого порядка с двумя переменными , Бюллетень символической логики, Vol.3, № 1 (март 1997 г.), стр. 53-69.
^ А.С. Кар, Эдвард Ф. Мур и Хао Ван. Entscheidungsproblem Сведена к случаю ∀ ∃ ∀ , 1962 г., отметив, что их формулы ∀ ∃ ∀ используют только три переменные.
^ Э. Гредель, М. Отто и Э. Розен. Логика двух переменных со счетом разрешима. , Труды двенадцатого ежегодного симпозиума IEEE по логике в информатике, 1997.
^ Гроэ, Мартин. «Логика конечных переменных в описательной теории сложности». Бюллетень символической логики 4.4 (1998): 345-398.

[1] Л. Хенкин. Логические системы, содержащие только конечное число символов , Отчет математического факультета Монреальского университета, 1967 г.

[2] Э. Гредель, П. Г. Колайтис и М. Варди, О проблеме принятия решения для логики первого порядка с двумя переменными , Бюллетень символической логики, Vol.3, № 1 (март 1997 г.), стр. 53-69.

[3] А.С. Кар, Эдвард Ф. Мур и Хао Ван. Entscheidungsproblem Сведена к случаю ∀ ∃ ∀ , 1962 г., отметив, что их формулы ∀ ∃ ∀ используют только три переменные.

[4] Э. Гредель, М. Отто и Э. Розен. Логика двух переменных со счетом разрешима. , Труды двенадцатого ежегодного симпозиума IEEE по логике в информатике, 1997.

[5] Гроэ, Мартин. «Логика конечных переменных в описательной теории сложности». Бюллетень символической логики 4.4 (1998): 345-398.

[1]

[2]

[3]

[4]

[5]