  We introduce a two-dimensional metric (interval) temporal logic whose
internal and external time flows are dense linear orderings. We provide a
suitable semantics and a sequent calculus with axioms for equality and
extralogical axioms. Then we prove completeness and a semantic partial
cut-elimination theorem down to formulas of a certain type.
