Строго позитивные фрагменты модальных и дескрипционных логик

В докладе будут рассматриваться слабые фрагменты модальной логики, называемые строго позитивными. Формулы строго позитивного модального языка представляют собой импликации вида A → B, где A и B построены из переменных и константы T (истина) с использованием лишь & и экзистенциальных модальностей (типа «ромб»). Интерес к таким фрагментам возник около 2010 года независимо в двух различных областях: в дескрипционной логике и в области приложений модальной логики в теории доказательств.
С точки зрения дескрипционной логики строго позитивные фрагменты соответствуют профилю OWL 2 EL известного языка онтологий OWL, в котором различные свойства онтологий распознаваемы за полиномиальное время. В области теоретико-доказательственных приложений такие фрагменты называются «исчисления рефлексий» и представляют собой удобное средство исследования независимых утверждений, так называемых схем рефлексии в формальной арифметике, и вычисления характеристических ординалов формальных теорий.
Таким образом, в обеих областях строго позитивные языки и логики соединяют простоту и эффективность с достаточными выразительными возможностями. В докладе мы расскажем о проблемах общего характера, связанных со строго позитивными логиками, и опишем некоторые их приложения.