|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Сети доказательства для исчисления Ламбека с одним делением и модальностью для ослабления, используемой только при отрицательной полярностистатья Электронная публикация
- Авторы: Пентус А.Е., Пентус М.Р.
- Журнал: ArXiv e-prints
- Номер: 1912.03739
- Год издания: 2019
- Первая страница: 1
- Последняя страница: 11
- Аннотация: В статье вводится вариант исчисления Ламбека, допускающего пустые антецеденты секвенций. В этом варианте используются две связки: левое деление и одноместная модальность, которая встречается только с отрицательной полярностью и разрешает ослабление в антецеденте секвенции. Определяется понятие сети доказательства для этого исчисления, подобное аналогичным сетям для обычного исчисления Ламбека и линейной логики. Доказывается, что произвольная заданная секвенция выводится в рассматриваемом исчислении тогда и только тогда, когда для неё существует сеть доказательства. Тем самым устанавливается критерий для проверки выводимости в этом исчислении в терминах существования графа с определёнными свойствами. При этом размер графа ограничен длиной секвенции.
- Добавил в систему: Пентус Мати Рейнович