Строго позитивная логика конечных линейных порядков, продолжение

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