This paper gives a broad account of the various sequent-based proof formalisms in the proof-theoretic literature. We consider formalisms for various modal and tense logics, intuitionistic logic, conditional logics, and bunched logics. After providing an overview of the logics and proof formalisms under consideration, we show how these sequent-based formalisms can be placed in a hierarchy in terms of the underlying data structure of the sequents. We then discuss how this hierarchy can be traversed using translations. Translating proofs up this hierarchy is found to be relatively easy while translating proofs down the hierarchy is substantially more difficult. Finally, we inspect the prevalent distinction in structural proof theory between 'internal calculi' and 'external calculi'. It is observed that these classes resist a rigorous separation, and we critically assess the properties that (calculi from) these classes are purported to possess.

翻译：本文广泛考察了证明论文献中各种基于矢列式的证明形式体系。我们考虑了多种模态逻辑、时态逻辑、直觉主义逻辑、条件逻辑以及束逻辑的形式体系。在概述所研究的逻辑及其证明形式体系后，我们展示了这些基于矢列式的形式体系如何根据底层矢列数据结构被纳入一个层级结构中。随后讨论了如何通过翻译遍历这一层级结构。我们发现，沿层级向上翻译证明相对容易，而向下翻译则困难得多。最后，我们审视了结构证明论中“内演算”与“外演算”的常见区分。观察到这些类别难以严格分隔，并批判性地评估了这些类别的演算所声称具备的属性。