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