Тип публикации: доклад, тезисы доклада, статья из сборника материалов конференций
Конференция: МАЛЬЦЕВСКИЕ ЧТЕНИЯ; Новосибирск; Новосибирск
Год издания: 2018
Аннотация: Унификационная проблема представляет собой возможность преобразовать фор- мулу в теорему после замены переменных [1]. Будем говорить, что формула .(p1, . . . , ps) унифицируема в L тогда и только тогда, когда существует подстановка (унификатор) . : pi 7> .i для каждой pi такая, что .(.1, . . . , .s) . L. Унификатор . формулы .(p1, Показать полностью. . . , ps) назовем более общим чем .1 в L (.1 .), если существует подстановка .2 такая, что для любой переменной pi . V ar(.): .1(pi) . .2(.(pi)) . L. Набор унификаторов CU формулы . называется полным в L, если для любого унификатора . формулы . найдется .1 . CU: . .1. Подстановка . называется проективным унификатором для .(p1, . . . , ps) в L, если выполняются оба следующих условия: (1) . (.) . L (т.е. . - унификатор для .); (2) . > [pi . . (pi)] . L для любой переменной pi . V ar(.). Исследуется унификация в предтабличных расширениях модальной логики S4, опи- санных Л. Л. Максимовой [2, 3], Л.Л. Эсакиа и В.Ю. Месхи [4]. Довольно изученными в этой связи являются логики PM1 и PM5 из набора, т. к. унификация в соответству- ющих им известных системах S4.3 и S5 соответственно рассматривалась в работах В.В. Рыбакова и В. Джика - в частности, последним была доказана ее проективность в обеих системах [5, 6]. Проблемы унификации для случаев PM2,PM3 и PM4 оста- ются открытыми. В докладе рассматриваются вопросы проективности, типа унификации в логиках, полных наборов и основных (граунд) унификаторов.
Журнал: МАЛЬЦЕВСКИЕ ЧТЕНИЯ
Номера страниц: 223
Издатель: Федеральное государственное бюджетное учреждение науки Институт математики им. С. Л. Соболева