Expressiveness and completeness of an interval tense logic.

Abstract

We present the syntax and semantics of an interval-based temporal logic which was defined by Halpern and Shoham. It is proved that this logic has a greater capacity to distinguish frames than any temporal logic based on points and we show that neither this nor any other finite set of operators can be functionally complete on the class of dense orders. In the last part of the paper we give sound and complete sets of axioms for several classes of structures. The methods employed in the paper show that it is rewarding to view intervals as points in a plane, in the style of two-dimensional modal logic.