论文标题
模态证明理论的旅程：从最小正常模态逻辑到离散的线性时间逻辑
A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
论文作者
论文摘要
扩展和推广2个时间的方法（Masini，1992），我们提出了K，D，T，S4 Spectrum中经典模态逻辑的顺序分解。通过调谐单个参数，即对规则的适用性构成限制，以统一的方式差异逻辑呈现系统。切割仅证明了一次，因为证明与产生不同系统的约束独立进行。还给出并证明了离散线性时间逻辑LTL的顺序演算。本文的leitmotiv是模态和一阶定量之间的形式类比。
Extending and generalizing the approach of 2-sequents (Masini, 1992), we present sequent calculi for the classical modal logics in the K, D, T, S4 spectrum. The systems are presented in a uniform way-different logics are obtained by tuning a single parameter, namely a constraint on the applicability of a rule. Cut-elimination is proved only once, since the proof goes through independently from the constraints giving rise to the different systems. A sequent calculus for the discrete linear temporal logic ltl is also given and proved complete. Leitmotiv of the paper is the formal analogy between modality and first-order quantification.
