Admissible Inference Rules in the Linear Logic of Knowledge and Time LTK
Erica Calardo Β· Logic Journal of IGPL Β· 2006
The paper investigates admissible inference rules for the multi-modal logic LTK, which describes a combination of linear time and knowledge. This logic is semantically defined as the set of all βπ―π¦-valid formulae, where βπ―π¦-frames are multi-modal Kripke-frames combining a linear and discrete representation of the flow of time with special S5-like modalities, defined at each time cluster and representing knowledge. We start by revising the effective finite model property in this particular case, while the central part of the paper is devoted to constructing special n-characterising models for LTK. Such structeres allow us to find an algorithm determining admissible inference rules in LTK; the main result of this work is that LTK is decidable with respect to inference rules.