Аннотация:

In this paper we study admissibility problem for non-linear temporal logic $L$. We consider a special generalization of projective formulas. Using this technique we find algorithm computing most general unifier for any given unifiable in $L$ formula. Logic $L$ is generated by family of all closed temporal models with compression property. Based on prepared technique, we prove that the admissibility problem and unification problem for $L$ are decidable.