证明逻辑的加标序列演算与反模型构造
Labeled Sequent Calculus and Countermodel Construction for Justification Logics
AI总结：
本文针对证明逻辑及混合模态-证明逻辑提出加标序列演算，内化Fitting模型语义，证明其弱子公式性质、规则可逆性等性质，建立可靠性完备性，给出可终止的证明搜索与反模型构造流程及模型对应关系。
摘要：
证明逻辑是一类类模态逻辑，为证明推理提供了框架。本文提出了适用于证明逻辑以及混合模态-证明逻辑的加标序列演算。我们采用Sara Negri提出的方法，将证明逻辑的克里普克式语义（即Fitting模型）内化到序列演算的语法中，以此构建加标序列演算。研究表明，我们提出的加标序列演算具备弱子公式性质，所有规则均可逆，且结构规则（弱化规则与收缩规则）以及切割规则都是可容许的。最后，本文证明了该演算的可靠性与完备性，同时验证了部分加标系统的证明搜索具有终止性。我们针对部分加标系统设计了一套流程，可为有效序列生成推导，为非有效序列生成反模型。此外，本文还在加标序列演算的语境下，给出了证明逻辑的模型对应关系。
英文摘要：
Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for hybrid modal-justification logics. Using the method due to Sara Negri, we internalize the Kripke-style semantics of justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculus. We show that our labeled sequent calculi enjoy a weak subformula property, all of the rules are invertible and the structural rules (weakening and contraction) and cut are admissible. Finally soundness and completeness are established, and termination of proof search for some of the labeled systems are shown. We describe a procedure, for some of the labeled systems, which produces a derivation for valid sequents and a countermodel for non-valid sequents. We also show a model correspondence for justification logics in the context of labeled sequent calculus.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
