Тип публикации: статья из журнала
Год издания: 2011
Идентификатор DOI: 10.1016/j.apal.2011.06.004
Ключевые слова: Unification, Linear temporal logic, Unification type
Аннотация: 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 aПоказать полностьюnd unifiable in LTL formula is projective. We also present an algorithm for constructing a most general unifier. (C) 2011 Elsevier B.V. All rights reserved.
Журнал: ANNALS OF PURE AND APPLIED LOGIC
Выпуск журнала: Vol. 162, Is. 12
Номера страниц: 991-1000
ISSN журнала: 01680072
Место издания: AMSTERDAM
Издатель: ELSEVIER SCIENCE BV