We define and study translations between the maximal class of analytic display calculi for tense logics and labeled sequent calculi, thus solving an open problem about the translatability of proofs between the two formalisms. In particular, we provide PTIME translations that map cut-free display proofs to and from special cut-free labeled proofs, which we dub 'strict' labeled proofs. This identifies the space of cut-free display proofs with a polynomially equivalent subspace of labeled proofs, showing how calculi within the two formalisms polynomially simulate one another. We analyze the relative sizes of proofs under this translation, finding that display proofs become polynomially shorter when translated to strict labeled proofs, though with a potential increase in the length of sequents; in the reverse translation, strict labeled proofs may become polynomially larger when translated into display proofs. In order to achieve our results, we formulate labeled sequent calculi in a new way that views rules as 'templates', which are instantiated with substitutions to obtain rule applications; we also provide the first definition of primitive tense structural rules within the labeled sequent formalism. Therefore, our formulation of labeled calculi more closely resembles how display calculi are defined for tense logics, which permits a more fine-grained analysis of rules, substitutions, and translations. This work establishes that every analytic display calculus for a tense logic can be viewed as a labeled sequent calculus, showing conclusively that the labeled formalism subsumes and extends the display formalism in the setting of primitive tense logics.

翻译：我们定义并研究了时态逻辑最大解析显示演算类与标记相继式演算之间的转换关系，从而解决了关于两种形式体系间证明可转换性的一个开放问题。特别地，我们提供了多项式时间转换算法，可将无切割显示证明与特殊的无切割标记证明（我们称之为"严格"标记证明）进行双向映射。这确立了无切割显示证明空间与一个多项式等价的标记证明子空间之间的对应关系，展示了两种形式体系内的演算如何实现多项式相互模拟。我们分析了该转换下证明的相对规模，发现显示证明转换为严格标记证明时会多项式缩短，但相继式长度可能增加；在反向转换中，严格标记证明转换为显示证明时可能多项式增大。为实现这些结果，我们以新方式构建标记相继式演算，将规则视为通过替换实例化得到规则应用的"模板"；同时首次在标记相继式形式体系中定义了原始时态结构规则。因此，我们的标记演算构建方式更贴近时态逻辑显示演算的定义范式，从而支持对规则、替换和转换进行更细粒度的分析。本工作证实每个时态逻辑的解析显示演算都可视为标记相继式演算，最终证明在原始时态逻辑框架下，标记形式体系包含并扩展了显示形式体系。