Logical consecutions in intransitive temporal linear logic of finite intervals.

*(English)*Zbl 1091.03002The problem of logical consequence in linear temporal logics is studied in terms of logical consecutions. A logical consecution (or inference rule) \(c\) is an expression \(\phi _{1}\),…, \(\phi _{n}\) / \(\psi \), where all \(\phi _{i}\) and \(\psi \) are formulas. An informal meaning of c is ‘\(\psi \) is a logical consequence of assumptions \(\phi _{1}\),…, \(\phi _{n}\)’. Valid and admissible temporal consecutions are introduced and it is proved that the class of admissible consecutions is a proper extension of the class of all valid consecutions. First the admissible consecutions are described of the intransitive linear temporal Tomorrow/Yesterday Logic TYL defined by intervals of natural numbers in a semantic manner – via consecutions valid on special constructive temporal Kripke/Hintikka models. Then it is shown that any temporal consecution has a reduced normal form, which is given in terms of temporal formulas of temporal degree at most 1. Using this and an enhanced semantic technique, an algorithm is constructed that recognizes consecutions admissible in TYL, that is, it is shown that TYL is decidable w.r.t. admissible consecutions.

Reviewer: Giacomo Bonanno (Davis)