Тип публикации: статья из журнала
Год издания: 2011
Идентификатор DOI: 10.1093/logcom/exq020
Ключевые слова: Temporal logic, admissible rules, bases for inference rules, Inference rules, Linear temporal logic, Structure and properties, Computability and decidability
Аннотация: The object of our study is the propositional linear temporal logic LTL with operations Until and Next. We deal with inference rules admissible in LTL. Earlier the decidability of LTL w.r.t. to admissibility was shown. That, in particular, allowed to suggest a recursive infinite basis for admissible rules. However, that result givesПоказать полностьюno information about the structure and properties of such basis, thereby not allowing to use it for inferences. The current article aims to cover this gap and to provide an explicit (infinite) basis for rules admissible in LTL.
Журнал: JOURNAL OF LOGIC AND COMPUTATION
Выпуск журнала: Vol. 21, Is. 2
Номера страниц: 157-177
ISSN журнала: 0955792X
Место издания: OXFORD
Издатель: OXFORD UNIV PRESS