Тип публикации: статья из журнала
Год издания: 2024
Идентификатор DOI: 10.33048/smzh.2024.65.115
Ключевые слова: modal logic, unification, Admissibility problem, Computation of unifiers, Projective formulas, Admissible rules, модальные логики, унификация, проблема допустимости, вычисление унификаторов, проективные формулы, допустимые правила
Аннотация: Изучаются проблемы унифицируемости и допустимости правил вывода для бесконечного класса модальных логик. Логики предполагаются разрешимыми, полными по Крипке и порождаемыми классами фреймов с наибольшими кластерами (в частности, такие логики расширяют модальную логику $S$4.2). Для любой такой логики $L$ и для любой формулы $\alpha$Показать полностью, унифицируемой $L$, эффективно строится некоторый унификатор $\sigma$ для $\alpha$ в $L$, проверяющий допустимость в $L$ любого данного правила вывода $\alpha/\beta$ с переключаемой главной модальностью для заключения правила $\beta$ (т. е. $\sigma$ решает проблему допустимости для всех таких правил вывода). We study unification and admissibility for an infinite class of modal logics. Conditions superimposed to these logics are to be decidable, Kripke complete, and generated by the classes of rooted frames possessing the greatest clusters of states (in particular, these logics extend modal logic S4.2). Given such logic $L$ and each formula $\alpha$ unifiable in $L$, we construct a unifier $\sigma$ for $\alpha$ in $L$, where $\sigma$ verifies admissibility in $L$ of arbitrary inference rules $\alpha/\beta$ with a switched-modality conclusions $\beta$ (i.e., $\sigma$ solves the admissibility problem for such rules).
Журнал: Сибирский математический журнал
Выпуск журнала: Т.65, №1
Номера страниц: 198-206
ISSN журнала: 00374474
Место издания: Новосибирск
Издатель: Сибирское отделение РАН, Институт математики им. С.Л. Соболева СО РАН