Projective formulas and unification in linear temporal logic LTLU

Описание

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

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

Персоны

  • Rybakov Vladimir (Manchester Metropolitan Univ, Dept Comp & Math, Manchester M1 5GD, Lancs, England; Siberian Fed Univ, Math Inst, Krasnoyarsk, Russia)