Полиномиальный алгоритм распознавания выводимости в строго позитивной логике линейных порядков

Строго позитивные логики описывают множества импликаций A->B, где A и B - модальные формулы, строящиеся лишь с помощью конъюнкции и модальностей типа "ромб" из переменных и константы "истина". Будет указан полиномиальный разрешающий алгоритм для строго позитивного фрагмента логики конечных иррефлексивных линейных порядков GL.3. До недавнего времени этот фрагмент рассматривался как возможная строго позитивная логика с co-NP полной проблемой выводимости, однако автору удалось опровергнуть эту гипотезу (по модулю P не = NP).