?
Бинарный предикат, транзитивное замыкание, две-три переменные: сыграем в домино?
Проблемы укладки домино являются удобным инструментом оценки алгоритмической сложности задач, возникающих в различных разделах математики, в том числе в логике. В работе описывается моделирование проблем домино с помощью средств языка логики предикатов, а также с помощью некоторых дополнительных средств, в том числе не выразимых элементарно. Это даёт возможность получить как простые доказательства уже известных фактов о неразрешимости проблемы выполнимости формул различных фрагментов логики предикатов, так и некоторые новые результаты. Так, известно, что проблема выполнимости формул логики предикатов, содержащих не более двух предметных переменных, алгоритмически разрешима; известно также, что свойство транзитивности бинарного отношения и операция композиции двух бинарных отношений могут быть выражены в языке первого порядка с использованием трёх переменных. В работе показано, что если добавить к языку первого порядка оператор проверки транзитивности бинарного отношения (или более сильное средство -- оператор транзитивного замыкания) и оператор композиции, то получим язык с сильно неразрешимой проблемой выполнимости формул от двух переменных, построенных в сигнатуре с одной бинарной предикатной буквой и равенством.