A decision procedure for nonperiodic sequents of the first-order linear temporal logic (Q1881801)

The author continues his research line about sequent systems for first-order linear temporal logic. Specifically, this paper builds upon Liet. Mat. Rink. 41, No. 4, 477--492 (2001; Zbl 1026.03012) and Liet. Mat. Rink. 41, No. 3, 338--361 (2001; Zbl 1019.03013), in which a deductive-based procedure for Horn-like sequents, so-called \(D_2\)-sequents, of first-order linear temporal logic was presented. The aim of this paper is to present a deduction-based decision procedure for nonperiodic \(D\)-sequents, which are obtained from elementary \(D_2\)-sequents by removing their periodicity condition (strictly nonperiodic and semiperiodic \(D\)-sequents are considered). Thus, the main contribution of the paper is to show that the periodicity condition on sequents is not essential to get a decision procedure. The structure of the paper is quite similar to that of the first paper cited above, the difference being that \(D\)-sequents, instead of \(D_2\)-sequents, are used: Firstly, the case of strictly nonperiodic \(D\)-sequents is considered; then, the decision procedure for \(D_2\)-sequents is adapted to work for semiperiodic \(D\)-sequents. Finally, an invariant decidable calculus \(D\)IN is used to prove the soundness and completeness of the calculus.