Разрешимость многомодальной линейной логики знания и времени LTK

Abstract

Thepaperinvestigates modal(temporal-model) logicsbased at a semantic approach with models combining knowledge and time. We introduce multi-modal logics LT Kr and LT Kir containing modalities for knowledge and time as the sets of all LT Kr -valid, and LT Kir -valid formulae for a class of special LT Kr frames, LT Kir -frames, respectively. The main results of this paper are theorems stating that LT Kr and LT Kir are decidable; we also give an explicit solving algorithm.

В представленной статье используется семантический подход к построению моделей, комбинирующихмодальности знания ивремени.Семантическивводятсямногомодальныелогики LT Kr и LT Kir , содержащие модальности знания и времени как множество формул, истинных на фреймах специального вида. Главным результатом работы являются теоремы об эффективной финитной аппроксимируемости и, как следствие, разрешимости данных логик.