О финитной аппроксимируемости и сложности логик сумм шкал Крипке

Мы рассмотрим операцию суммирования шкал Крипке, в которой индексы шкал-слагаемых также являются элементами некоторой шкалы. Многие модальные логики могут быть описаны в терминах сумм, в которых слагаемые — это шкалы более простой (в том или ином смысле) логики.
Оказывается, что во многих случаях логика сумм наследует финитную аппроксимируемость и разрешимость логики слагаемых. Общее наблюдение состоит в том, что логика сумм по нётеровым (в частности, конечным) порядкам сводится к логике слагаемых. Например, логика S4 оказывается сводима к логике S5, GL сводится к классической логике, логика слабой транзитивности wK4 — к логике неравенства.
Более того, сведение к логике слагаемых — это сведение по Тьюрингу, в котором алгоритм работает с полиномиальным ограничением на зону вычисления. Из этого следует разрешимость в классе PSPACE многих модальных логик.