Эта публикация цитируется в
1 статье
Алгебро-логические методы в информатике и искусственный интеллект
Глобально допустимые правила вывода
В. В. Римацкий Сибирский федеральный университет, Красноярск, Российская Федерация
Аннотация:
Задание базовых правил вывода имеет фундаментальное значение для логики. Наиболее общим вариантом возможных правил вывода являются допустимые правила вывода: в логике
$L$ правило вывода допустимо, если множество теорем
$L$ замкнуто относительно данного правила. Изучение допустимых правил вывода было стимулировано проблемой Фридмана: существует ли алгоритм распознавания допустимости правила вывода в интуиционистской логике? Для широкого класса неклассических логик проблема разрешимости по допустимости правил вывода была решена в сер. 1980-х. К проблеме А. Кузнецова (1975) восходит другой способ описания всех допустимых в логике правил: задание некоторого (конечного) набора допустимых правил, из которого все остальные допустимые в логике правила будут выводиться как следствия, т. е. задание (конечного) базиса. Большинство базовых неклассических логик не имеют конечного базиса для допустимых правил вывода. В начале 2000-х гг. для большинства базовых неклассических логик и некоторых табличных логик проблема Фридмана – Кузнецова была решена с помощью описания явного базиса для допустимых правил.
Следующим этапом изучения допустимых правил вывода неклассических логик можно считать понятие глобально допустимого правила вывода.
Глобально допустимыми правилами в логике $L$ называем те правила вывода, которые допустимы сразу во всех (финитно аппроксимируемых) расширениях данной логики. Представленная работа посвящена изучению глобально допустимых правил логики
$S4$. Были получены условия глобальной допустимости в логике
$S4$, построена характеристическая (универсальная) модель (проверка глобальной допустимости сводится к проверке истинности правила на ее подмоделях), описаны базис (из него выводятся все глобально допустимые правила) и антибазис (из него выводятся все правила, недопустимые глобально в
$S4$).
Ключевые слова:
модальная логика, фрейм и модель Крипке, допустимое правило вывода, глобально допустимые правила вывода.
УДК:
510.643; 517.11
MSC: 03F25,
03B35 Поступила в редакцию: 04.07.2022
Исправленный вариант: 03.08.2022
Принята в печать: 01.09.2022
DOI:
10.26516/1997-7670.2022.42.138