Перевод названия: 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Все результаты являются новыми, открывают дополнительные возможности успешного выполнения проекта и находятся на уровне самых современных исследований международного уровня. According to the plan of the second stage of the project, deductive systems for nonstandard logics and semantic tools of nonstandard logics have been investigated. The primary attention has been paid to the admissible inference rules. pWe study quasi-characterizing inference rules which were introduced into consideration by A.Citkin (1977). The main result of our paper consists of a complete description of all quasi-characteristic rules which are self-admissible. It turns out that a rule is self-admissible iff the frame of the algebra generating this rule is not rigid. pWe also prove that self-admissible rules are always admissible in canonical, in a sense, logics S4 or IPC regarding the type of algebra generating rules. We give a very simple and transparent criteria (and algorithms) for recognizing whether formulas are unifiable in modal logics, and present a construction of simplest unifiers for unifiable formulas. pA description of "anti-basis" for not unifiable formulas is obtained: we found a set of regular and simple formulas of modal degree one B such that as soon as a formula is not unifiable we can derive from this formula a precisely specified formula from B. Then we consider passive inference rules, a rule is passive if its premise is not unifiable. Applying obtained results concerning unification we describe in precise bases for passive rules in all modal logics considered, in particular in all modal logics extending S4. pThe series of bimodal logics S52C+font face="symbol"w/fontn1, S52C+font face="symbol"w/fontn2 of finite depth and width was studied. It was proved that the intersection of logics from each family coisides with bimodal logic S52C. The lattice L of subvarieties of certain variety V of bimodal algebras was studied. It was proved that the lattice L has not infinite descending chains, the free algebra of any variety from the lattice L has the finite bases of identities and its universal theory is decidable. The free algebra of any proper subvariety of variety V is locally finite. The free algebra of variety V is not locally finite. pA base of quasi-identities for any variety from the lattice L was constructed. The equations in free topobulean algebras was investigated. It was proved that for any tabular and pretabular logic the quasi-equational theory of its free algebra in signature extended by constants is decidable. An algorithm of determining the admissibility of inference rules for logic LinTGrz is constructed. pSome individual results for logics of width 2 are obtained. It was studied the inference rules with metavariables for all pretabular modal logics over S4. An algorithm of choice the admissible inference rules for these logics was constructed. For modal logics of depth 2 it was proved that they have finite bases for admissible inference rules. It was proved that an extension of tabular logic font face="symbol"l/font over S4 has finite bases for admissible inference rules if font face="symbol"l/font has finite bases for admissible inference rules. pIn sum we published and sent for publication 19 papers (taking into account papers which were sent to journals before 1997). Head of the project V.V.Rybakov published the book emAdmissible Inference Rules for Logical Systems/em, Elsevier Sci. Publishers (North-Holland, Amsterdam-New-York), 1997, in volume 617pp. pAll obtained results of the project are new, they give a good promising for further succeed fulfillment of the project, and are on the international level of modern research.