Тип публикации: статья из журнала
Год издания: 2014
Идентификатор DOI: 10.1093/jigpal/jzu005
Ключевые слова: linear temporal logic, unification, computation of unifiers, projective formulas, admissible rules
Аннотация: We study projectivity in temporal linear logic LTL with the aim to solve unification problem. Earlier [34] it was shown that not all formulas unifiable in LTL are projective. Therefore here we consider Until-fragment LTLU of LTL. By idea borrowed from [33] we find a short proof that all formulas unifiable at LTLU are projective. This implies that any unifiable in LTLU formula has most general unifier (a procedure to compute it is provided) and solves the open admissibility problem for LTLU. Also we recall that similar construction works for all modal linear logics extending S4.3.
Издание
Журнал: LOGIC JOURNAL OF THE IGPL
Выпуск журнала: Vol. 22, Is. 4
Номера страниц: 665-672
ISSN журнала: 13670751
Место издания: OXFORD
Издатель: OXFORD UNIV PRESS
Персоны
- Rybakov Vladimir (Manchester Metropolitan Univ, Dept Comp & Math, Manchester M1 5GD, Lancs, England; Siberian Fed Univ, Math Inst, Krasnoyarsk, Russia)
Вхождение в базы данных
Информация о публикациях загружается с сайта службы поддержки публикационной активности СФУ. Сообщите, если заметили неточности.