Аннотация:
В докладе рассматриваются два расширения исчисления Ламбека
с помощью одноместных связок (модальностей). В первом
расширении для формул под знаком модальности действуют
правила ослабления, сокращения и перестановки, во втором -
только сокращения и перестановки. (В исходном исчислении Ламбека
этих правил нет.) Первая модальность соответствует
экспоненциальному оператору некоммутативной линейной логики,
вторая же имеет лингвистический смысл. Для обоих расширений
доказывается алгоритмическая неразрешимость проблемы
выводимости.
|
