Неразрешимость теории алгебр Клини с условиями коммутативности

В работе 2002 г. Декстер Козен определил уровни алгоритмической сложности для теорий алгебр Клини, как в общем, так и в *-непрерывном случае — от эквациональных теорий до хорновых, т.е. задач следования из конечных множеств гипотез. В частности, для выводимости из гипотез вида $xy = yx$, где $x$ и $y$ — переменные, в *-непрерывном случае была доказана $\Pi^0_1$-полнота. Такие гипотезы называются условиями коммутативности. Определение сложности задачи следования из конечных множеств условий коммутативности на классе всех (не обязательно *-непрерывных) алгебр Клини оставалось открытым вопросом. В докладе будет изложено его решение — доказательство $\Sigma^0_1$-полноты данной задачи. При доказательстве используется кодирование циклической работы машин Тьюринга и соображения эффективной неотделимости.