标题： 直觉主义模态逻辑的正当性逻辑（扩展技术报告） 显示英文标题

标题： Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)

摘要： 证明逻辑是对模态逻辑的解释；方框通过实现定理被形式地用证明项替代。 这可以通过使用无切割的证明系统来实现，例如使用序列、超序列或嵌套序列演算。 在构造性模态逻辑中，方框和菱形是解耦的，并不是德摩根对偶。 Kuznets、Marin 和 Stra{\ss }burger 通过引入称为满足者的新的项，使菱形显式化，为构造性模态逻辑 CK 及其一些扩展提供了证明对应物。 我们继续这项工作，为 Fischer Servi 的直觉主义模态逻辑 IK 及其添加 t 和 4 公理的扩展提供一个证明对应物。 我们：扩展证明项的语法以适应直觉主义模态逻辑的附加公理；提供这些证明逻辑的公理化；使用由 Stra{\ss }burger 引入的无切割嵌套序列系统，提供一种句法实现过程。 显示英文摘要

摘要： Justification logics are an explication of modal logic; boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system e.g. using sequent, hypersequent or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Kuznets, Marin and Stra{\ss}burger provide a justification counterpart to constructive modal logic CK and some extensions by making diamonds explicit by introducing new terms called satisfiers. We continue the line of work to provide a justification counterpart to Fischer Servi's intuitionistic modal logic IK and its extensions with the t and 4 axioms. We: extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic; provide an axiomatisation of these justification logics; provide a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic introduced by Stra{\ss}burger.