Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
6424846 | Annals of Pure and Applied Logic | 2011 | 10 Pages |
Abstract
We prove that a propositional Linear Temporal Logic with Until and Next (LTL) 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.
⺠We study unification problem for linear temporal logic LTL. ⺠We prove that every unifiable in LTL formula has a most general unifier. ⺠We also construct an algorithm building most general unifiers. ⺠This algorithm solves the unification problem in LTL.
Related Topics
Physical Sciences and Engineering
Mathematics
Logic
Authors
Sergey Babenyshev, Vladimir Rybakov,