Projective formulas and unification in linear temporal logic LTLU
Vladimir Vladimirovich Rybakov · Logic Journal of IGPL · 2014
We study projectivity in temporal linear logic LTL with the aim to solve unification problem. Earlier [34] it was shown that not all formulas unifiable in LTL are projective. Therefore here we consider Until-fragment LTLU of LTL. By idea borrowed from [33] we find a short proof that all formulas unifiable at LTLU are projective. This implies that any unifiable in LTLU formula has most general unifier (a procedure to compute it is provided) and solves the open admissibility problem for LTLU. Also we recall that similar construction works for all modal linear logics extending S4.3.