1.  32
    Unification in Linear Temporal Logic LTL.Sergey Babenyshev & Vladimir Rybakov - 2011 - Annals of Pure and Applied Logic 162 (12):991-1000.
    We prove that a propositional Linear Temporal Logic with Until and Next has unitary unification. Moreover, for every unifiable in LTL formula A there is a most general projective unifier, corresponding to some projective formula B, such that A is derivable from B in LTL. On the other hand, it can be shown that not every open and unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier.
    Direct download (4 more)  
    Export citation  
    Bookmark   11 citations  
  2.  4
    Behavioral Equivalence of Hidden K -Logics: An Abstract Algebraic Approach.Sergey Babenyshev & Manuel A. Martins - 2016 - Journal of Applied Logic 16:72-91.