论文标题
标记有定量模态逻辑的计算有明确的描述
Labelled calculi for quantified modal logics with definite descriptions
论文作者
论文摘要
我们介绍了具有确定描述的量化模态逻辑的标记序列结石。我们证明这些结石具有G3式骨的良好结构特性。特别是，所有规则都是可逆的，弱化和收缩都是可接受的，并且可以接受。最后，我们表明每个演算给出了相应模型类别中有效性的证明理论表征。
We introduce labelled sequent calculi for quantified modal logics with definite descriptions. We prove that these calculi have the good structural properties of G3-style calculi. In particular, all rules are height-preserving invertible, weakening and contraction are height-preserving admissible and cut is admissible. Finally, we show that each calculus gives a proof-theoretic characterization of validity in the corresponding class of models.
