Combining linear-time temporal logic with constructiveness and paraconsistency (Q975875)

The linear-time temporal logic (based on classical logic) is known to be useful for expressing temporal reasoning in computer science. From this viewpoint it is interesting to combine linear time with other aspects such as constructiveness or inconsistency-tolerance. In fact, it has been pointed out by Maier that certain intuitionistic linear-time temporal logic admits an elegant characterization of safety and liveness properties, where the logic is presented there in an algebraic setting. This paper provides Gentzen-type systems for intuitionistic and paraconsistent bounded linear-time temporal logics, respectively. Their time domain is bounded by a fixed positive integer, so that the logics are shown to enjoy faithful embeddings into intuitionistic logic and Nelson's paraconsistent logic, respectively, while almost all useful temporal axioms are available. The authors establish for them some fundamental properties such as completeness with respect to Kripke semantics, cut-elimination, and decidability. They are also formulated in natural deduction systems with normalization as well as in sound and complete display calculi.