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

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

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

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

Аннотация: Согласно основной направленности и плану второго этапа исследовались дедуктивные системы нестандартного логического вывода и семантический аппарат нестандартных логик. pОсновное внимание было уделено допустимым правилам вывода. Изучаются квази-характеристические правила вывода введённые Циткиным (1977). Основной результат состоит в полном описании всех квази-характеристических правил, которые являются самоприменимыми. Оказывается, что такое правило самоприменимо тогда и только тогда, когда шкала алгебры, порождающей данное правило не является жёсткой. pТакже показано, такие правила всегда самоприменимы в логиках S4 и IPC в соответствии с типом алгебры, порождающей данное правило. Дан очень простой и ясный критерий (и алгоритм) для распознавания будут ли формулы унифицируемы в модальных логиках. pПредложена также конструкция простейших унификаторов для унифицируемых формул. Получено описание "анти-базиса" для неунифицируемых формул: найдено множество B регулярных и простых формул модальной степени один, такое, что для каждой неунифицируемой формулы можно вывести из неё вполне определённую формулу из B. pДалее рассмотрены пассивные правила вывода, правило пассивно, если его посылка не унифицируема. Результаты касающиеся унификации дали возможность построить базисы для пассивных правил во всех рассмотренных модальных логиках, в частности во всех расширениях S4. pРассмотрены серии бимодальных логик S52C+font face="symbol"w/fontn1, S52C+font face="symbol"w/fontn2 конечной ширины и глубины. Доказано, что пересечение логик каждого из семейств совпадает с бимодальнй логикой S52C. pРассмотрена решетка L подмногообразий некоторого многообразия V бимодальных алгебр. Показано, что решетка L не имеет бесконечных убывающих цепей, свободная алгебра любого многообразия из решетки L имеет конечный базис тождеств и её универсальная теория разрешима. Свободная алгебра любого собственного подмногообразия многообразия V локально конечна, свободная алгебра многообразия V не является локально конечной. Для свободной алгебры любого многообразия из решетки L указан базис квазитождеств. pРассмотрены уравнения в свободных топобулевых алгебрах. Доказано, что для любой табличной и предтабличной логики квазиэквациональная теория свободной алгебры в сигнатуре, расширенной константами, разрешима. Построен алгоритм определения допустимости правил вывода для логики LinTGrz. Получены частичные результаты для логик ширины 2. pРассматривались правила вывода с метапеременными для всех предтабличных модальных логик (над S4), как для случая локально конечных логик, так и для единственного не локально конечного случая - логики PM1. Кроме того, показано, что все модальные логики глубины 2 имеют конечные базисы для допустимых правил вывода. pИсследованы табличные логики, являющиеся расширением S4 и имеющие конечный базис допустимых правил вывода, показано, что их расширения имеют конечный базис допустимых правил вывода. pСуммарно за 1997г. коллективом опубликовано и сдано печать 19 работ по теме (с учетом работ сданных в печать до 1997г.). Руководитель проекта В.В.Рыбаков опубликовал книгу Admissible Inference Rules for Logical Systems объемом 617 стр. Напечатанной в изд. сист. LaTeX, 10pt. в издательство Elsevier Sci. Publishers (North-Holland, Amsterdam-New-York), 1997г. pВсе результаты являются новыми, открывают дополнительные возможности успешного выполнения проекта и находятся на уровне самых современных исследований международного уровня.

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

Авторы

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

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

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

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