Non-unifiability in linear temporal logic of knowledge with multi-agent relations

Abstract

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.