Аннотация:The paper is devoted to the study of the unification problem in the linear temporal logic of knowledge with multi-agent relations (denoted in the sequel as LFPK). This logic is based on frames (models) with time points represented by integer numbers from Z and the information clusters Ci for i in Z with multi-agent accessibility relations Ri. The first main result is a theorem describing a criterion for formulas to be not unifiable in LFPK. The second one is a construction of a basis for all inference rules passive in LFPK.
Ключевые слова:unification, modal temporal logic, passive inference rules, Институт математики и фундаментальной информатики, Институт космических и информационных технологий, ИМиФИ, икит, сфу
