Нестандартные логические системы и правила вывода

Перевод названия: Nonstandard Logical Systems and Inference Rules.

Тип публикации: отчёт о НИР

Год издания: 1996

Аннотация: Согласно основной направленности и плану второго этапа исследовались дедуктивные системы нестандартного логического вывода и семантический аппарат нестандартных логик.

Основное внимание было уделено допустимым правилам вывода. Изучаются квази-характеристические правила вывода введённые Циткиным (1977). Основной результат состоит в полном описании всех квази-характеристических правил, которые являются самоприменимыми. Оказывается, что такое правило самоприменимо тогда и только тогда, когда шкала алгебры, порождающей данное правило не является жёсткой.

Также показано, такие правила всегда самоприменимы в логиках S4 и IPC в соответствии с типом алгебры, порождающей данное правило. Дан очень простой и ясный критерий (и алгоритм) для распознавания будут ли формулы унифицируемы в модальных логиках.

Предложена также конструкция простейших унификаторов для унифицируемых формул. Получено описание "анти-базиса" для неунифицируемых формул: найдено множество <i>B</i> регулярных и простых формул модальной степени один, такое, что для каждой неунифицируемой формулы можно вывести из неё вполне определённую формулу из <i>B</i>.

Далее рассмотрены пассивные правила вывода, правило пассивно, если его посылка не унифицируема. Результаты касающиеся унификации дали возможность построить базисы для пассивных правил во всех рассмотренных модальных логиках, в частности во всех расширениях S4.

Рассмотрены серии бимодальных логик S52C+wn1, S52C+wn2 конечной ширины и глубины. Доказано, что пересечение логик каждого из семейств совпадает с бимодальнй логикой S52C.

Рассмотрена решетка L подмногообразий некоторого многообразия V бимодальных алгебр. Показано, что решетка L не имеет бесконечных убывающих цепей, свободная алгебра любого многообразия из решетки L имеет конечный базис тождеств и её универсальная теория разрешима. Свободная алгебра любого собственного подмногообразия многообразия V локально конечна, свободная алгебра многообразия V не является локально конечной. Для свободной алгебры любого многообразия из решетки L указан базис квазитождеств.

Рассмотрены уравнения в свободных топобулевых алгебрах. Доказано, что для любой табличной и предтабличной логики квазиэквациональная теория свободной алгебры в сигнатуре, расширенной константами, разрешима. Построен алгоритм определения допустимости правил вывода для логики LinTGrz. Получены частичные результаты для логик ширины 2.

Рассматривались правила вывода с метапеременными для всех предтабличных модальных логик (над S4), как для случая локально конечных логик, так и для единственного не локально конечного случая - логики PM1. Кроме того, показано, что все модальные логики глубины 2 имеют конечные базисы для допустимых правил вывода.

Исследованы табличные логики, являющиеся расширением S4 и имеющие конечный базис допустимых правил вывода, показано, что их расширения имеют конечный базис допустимых правил вывода.

Суммарно за 1997г. коллективом опубликовано и сдано печать 19 работ по теме (с учетом работ сданных в печать до 1997г.). Руководитель проекта В.В.Рыбаков опубликовал книгу Admissible Inference Rules for Logical Systems объемом 617 стр. Напечатанной в изд. сист. LaTeX, 10pt. в издательство Elsevier Sci. Publishers (North-Holland, Amsterdam-New-York), 1997г.

Все результаты являются новыми, открывают дополнительные возможности успешного выполнения проекта и находятся на уровне самых современных исследований международного уровня.

Ссылки на полный текст

Авторы

  • Рыбаков В.В. (Красноярский Государственный Университет (КрасГУ))
  • Бабенышев С.В. (Красноярский Государственный Университет (КрасГУ))
  • Безгачева Ю.В. (Красноярский Государственный Университет (КрасГУ))
  • Голованов М.И. (Красноярский Государственный Университет (КрасГУ))
  • Кияткин В.Р. (Красноярский Государственный Университет (КрасГУ))
  • Римацкий В.В. (Красноярский Государственный Университет (КрасГУ))

Вхождение в базы данных

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.