Тип публикации: статья из журнала
Год издания: 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. ThПоказать полностьюis 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