Rules admissible in transitive temporal logic TS4, sufficient condition

The paper1 develops a technique for computation inference rules admissible in temporal logic TS4. The problem whether there exists an algorithm recognizing inference rules admissible in TS4 is a long-standing open problem. The logic TS4 has neither the extension property nor the co-cover property which previously were central instruments for construction decision algorithms for admissibility in modal logics (e.g. reflexive and transitive modal logic S4). Our paper uses a linear-compression property, a zigzag-ray property and a zigzag stretching property which hold for TS4. The main result of the paper is a sufficient condition for admissibility inference rules in TS4. It is shown that all rules which are valid in special finite models (with an effective upper bound on size) must be admissible in TS4.