Сибирский федеральный университет

Перевод названия: Проблема унификации в логике Нельсона N4

Тип публикации: статья из журнала

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

Ключевые слова: unification, Vorob'ev translation, трансляция Воробьева, Nelson's logic, Strong negation, complete sets of unifiers, decidability, логика Нельсона, сильное отрицание, полное множество унификаторов, разрешимость

Аннотация: We consider the unification problem for formulas with coefficients in the Nelson’s paraconsitent logic N4. By presence coefficients (parameters) the problem is quite not trivial and challenging (yet what makes the problem for N4 to be peculiar is missing of replacement equivalents rule in this logic). It is shown that the unification problem in N4 is decidable for ?-free formulas. We also show that there is an algorithm which computes finite complete sets of unifiers (so to say - all best unifiers) for unifiable in N4 ?-free formulas (i.e. any unifier is equivalent to a substitutional example of a unifier from this complete set). Though the unification problem for all formulas (not ?-free formulas) remains open.

Журнал: Сибирские электронные математические известия

Выпуск журнала: Т.11, №

Номера страниц: 434-443

ISSN журнала: 18133304

Место издания: Новосибирск

Издатель: Федеральное государственное бюджетное учреждение науки Институт математики им. С.Л. Соболева Сибирского отделения Российской академии наук

• Odintsov S.P. (Sobolev Institute of Mathematics)
• Rybakov V.V. (School of Computing, Mathematics and DT, Manchester Metropolitan University)

• РИНЦ (eLIBRARY.RU) (цитирований 1)
• Ядро РИНЦ (eLIBRARY.RU)
• Список ВАК
• Scopus