Decidability of $\Delta$-equivalence problem for monadic logic programs

В работе изучается $\Delta$-эквивалентность монадических логических прорамм (логических программ, содержащих только монадические функциональные и предикатные символы). Программы называются $\Delta$-эквивалентными, если множества логически следующих из них запросов совпадают. Показано, что в отличие от общего случая $\Delta$-эквивалентность монадических программ разрешима. Наше доказательство использует разрешимость монадической логики Рабина для функций следования второго порядка.