Unification in linear temporal logic LTL

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

Год издания: 2011

Идентификатор DOI: 10.1016/j.apal.2011.06.004

Ключевые слова: Unification, Linear temporal logic, Unification type, Linear temporal logic, Unification, 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 and 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)

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

Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.

Вы можете отметить интересные фрагменты текста, которые будут доступны по уникальной ссылке в адресной строке браузера.