We introduce the logic QKSD which is a normal multi-modal logic over finitely many modalities that additionally supports bounded quantification of modalities. An important feature of this logic is that it allows to quantify over the information components of systems and, hence, can be used to derive justifications. We compare the proposed logic with Artemov's justification logic and also report on a prototypical implementation of a satisfiability solver of this logic and show some examples.
翻译:我们引入了逻辑QKSD(QKSD),这是一个通常的多模式逻辑,它超越了有限的多种模式,这些模式进一步支持对模式进行限制性量化,这一逻辑的一个重要特征是,它允许对系统的信息组成部分进行量化,从而可以用来提出理由。我们比较了拟议的逻辑和Artemoov的逻辑解释,还报告了这一逻辑的相对性解决方案的原型实施,并列举了一些例子。