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