Минимальные модели и сложность фрагментов логики доказательств

В работе описан достаточно выразительный синтаксический фрагмент логики доказательств $LP$ С. Н. Артемова, который принадлежит классу $NP$, т.е. существенно проще всей логики. Он состоит из всех теорем $LP$, являющихся монотонными булевыми комбинациями квазиатомарных формул. Предложен новый разрешающий алгоритм, использующий новую независимую формализацию квазиатомарного фрагмента $LP$.
Библиогр. 4.