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

Перевод названия: Проблема унификации в логике Нельсона 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. Рассматривается проблема унификации формул с коэффициентами в паранепротиворечивой логике Нельсона {\bf N4}. Присутствие коэффициентов делает эту проблему для {\bf N4} очень сложной, что усугубляется отсутствием правила замены эквивалентных в данной логике. Показано, что проблема унификации в {\bf N4} разрешима для формул без сильного отрицания. Также установлено, что есть алгоритм, который вычисляет конечное полное множество унификаторов (можно сказать, множество всех наилучших унификаторов) для унифицируемых в {\bf N4} формул, не содержащих сильного отрицания, т.е. каждый унификатор эквивалентен частному случаю унификатора из данного полного множества. Тем не менее, проблема унификации для произвольных формул остается открытой.

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

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

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

ISSN журнала: 18133304

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

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

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

• Scopus
• Web of Science Core Collection
• Ядро РИНЦ (eLIBRARY.RU)
• Список ВАК