## Constructive Linear-Time Temporal Logic: Proof Systems and Kripke Semantics

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.

### Abstract

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.

### PDF file(s)