Multiagent temporal logics, unification problems, and admissibilities

Under study is the temporal multiagent logic with different intervals of lost time which are individual for each of the agents. The logic bases on the frames with principal basic sets on all naturals $N$ as temporal states, where each agent $j$ can have their own proper sets $X_j$ of inaccessible (lost, forgotten) temporal states ($X_j \subset N$ for all $j \in J$). The unification problem and the problem of the algorithmic recognition of admissible inference rules are the main mathematical problems of the paper. The solution of the unification problem consists in finding a finite computable set of formulas which is a complete set of unifiers. The problem is solved by the Ghilardi technique of projective formulas. We prove that every formula unifiable in this logic is projective and provide some algorithm constructing its projective unifier, which solves the unification problem. This makes it possible to solve the open problem of the algorithmic recognition of admissible rules. The article ends with some generalization of the definition of projective formulas—weakly projective formulas—and exhibits an easy example of their application.