Unification in linear temporal logic LTL

Описание

Тип публикации: статья из журнала

Год издания: 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

Авторы

  • Babenyshev S. (Department of Computing and Mathematics,Manchester Metropolitan University)
  • Rybakov V. (Institute of Mathematics,Siberian Federal University)

Вхождение в базы данных