Сложность исчисления Ламбека с одним делением и модальностью для ослабления, используемой только при отрицательной полярностистатья
Статья опубликована в журнале из списка RSCI Web of Science
Статья опубликована в журнале из перечня ВАК
Статья опубликована в журнале из списка Web of Science и/или Scopus
Дата последнего поиска статьи во внешних источниках: 8 апреля 2022 г.
Аннотация:В статье рассматривается вариант исчисления Ламбека, допускающего пустые антецеденты секвенций. В этом варианте используются две связки: левое деление и одноместная модальность, которая встречается только с отрицательной полярностью и разрешает ослабление в антецеденте секвенции. Определяется понятие сети доказательства для этого исчисления, подобное аналогичным сетям для обычного исчисления Ламбека и линейной логики. Доказывается, что произвольная заданная секвенция выводится в рассматриваемом исчислении тогда и только тогда, когда для неё существует сеть доказательства. Найден быстрый (полиномиальный по времени) алгоритм, устанавливающий, выводима ли произвольная данная секвенция в рассматриваемом исчислении.