
AbstractWe investigate logical consequence in temporal logics in terms of logical consecutions, i.e., inference rules. First, we discuss the question: what does it mean for a logical consecution to be ‘correct’ in a propositional logic. We consider both valid and admissible consecutions in linear temporal logics and discuss the distinction between these two notions. The linear temporal logicLDTL, consisting of all formulas valid in the frame 〈L≤, ≥〉 of all integer numbers, is the prime object of our investigation. We describe consecutions admissible inLDTLin a semantic way—via consecutions valid in special temporal Kripke/Hintikka models. Then we state that any temporal inference rule has a reduced normal form which is given in terms of uniform formulas of temporal degree 1. Using these facts and enhanced semantic techniques we construct an algorithm, which recognizes consecutions admissible inLDTL. Also, we note that using the same technique it follows that the linear temporal logicL(N) of all natural numbers is also decidable w.r.t. inference rules. So, we prove that both logicsLDTLandL(N) are decidable w.r.t. admissible consecutions. In particular, as a consequence, they both are decidable (known fact), and the given deciding algorithms are explicit.
inference, temporal logic, consecutions, admissible rules, inference rules, linear temporal logic, logical consequence
inference, temporal logic, consecutions, admissible rules, inference rules, linear temporal logic, logical consequence
| citations This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 55 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Top 10% | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Top 10% | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Top 10% |
