Admissible inference rules in the linear logic of knowledge and time \(\mathrm{LTK}_r\) with intransitive time relation (Q498234)

The paper presents an investigation on a linear logic of knowledge and time with intransitive time relation \(\mathrm{LTK}_r\). This is a multi-modal logic obtained by adding epistemic and temporal operators to the classical propositional logic. The logic is formulated semantically in the language with three kinds of modal operators: \(\square_T\), \(\square_\sim\) and \(\square_i\) (\(1\leq i \leq k\)), where \(\square_T A\) means that \(A\) is true at the moment of consideration, and will be true at every subsequent moment, \(\square_\sim A\) means that \(A\) is just true at the moment, and \(\square_i A\) means that \(A\) is true at all information states available to the agent \(i\). These operators are defined through the corresponding accesibility relations. The main result of the paper consists in the demonstration of the decidability of \(\mathrm{LTK}_r\) with respect to the admissibility of inference rules. To this effect, the authors construct an algorithm allowing for any given inference rule to decide, whether it is admissible in \(\mathrm{LTK}_r\) or not. The algorithm is based on a special Kripke-frame construction that consists of chains of proper \(R_\sim\)-clusters or of a single point.