By Kensuke Kojima and Atsushi Igarashi. Information and Computation. To appear. An earlier version titled "On Constructive Linear-Time Temporal Logic" appeared in Proceedings of Intuitionistic Modal Logic and Applications Workshop, Pittsburgh, PA, June, 2008.
In this paper we study a version of constructive linear-time temporal logic (LTL) with the ``next'' temporal operator. The logic is originally due to Davies, who has shown that the proof system of the logic corresponds to a type system for binding-time analysis via the Curry-Howard isomorphism. However, he did not investigate the logic itself in detail; he has proved only that the logic augmented with negation and classical reasoning is equivalent to (the ``next'' fragment of) the standard formulation of classical linear-time temporal logic. We give natural deduction and Kripke semantics for constructive LTL with conjunction and disjunction, and prove soundness and completeness. Distributivity of the ``next'' operator over disjunction is rejected from a computational viewpoint. We also give a formalization by sequent calculus and its cut-elimination procedure.
$Date: $