论文标题
通过嵌套序列的角度逻辑自动推理自动推理
Automating Reasoning with Standpoint Logic via Nested Sequents
论文作者
论文摘要
在知识整合的背景下，立场逻辑是最近提出的形式主义，它提倡采用多方面的方法，允许以各种不同的和可能相互冲突的角度来推理，而不是强迫他们的统一。在本文中，我们引入了嵌套的序列计算，以进行命题的角度逻辑 - 防止树的系统，这些系统操纵树的节点是公式的多组，并展示了如何通过非确定性证明搜索算法来自动化观点的观点。为了获得最坏情况的复杂性 - 最佳的证明搜索，我们在嵌套序列的上下文中介绍了一种新技术，称为“着色”，其中包括将公式作为输入，猜测其子形式的某些颜色，然后在嵌套的序列中进行嵌套的序列搜索。我们的技术使我们能够确定conp的观点公式的有效性，因为证明搜索仅产生相对于输入的每个允许着色的部分证明。我们展示了如何将所有部分证据融合在一起以在输入有效时构建完整的证明，以及当输入无效时，如何将某些部分证据转换为反模型。这些“证书”（即证明和反模型）可以作为对输入有效性的（在）有效性的解释。
Standpoint logic is a recently proposed formalism in the context of knowledge integration, which advocates a multi-perspective approach permitting reasoning with a selection of diverse and possibly conflicting standpoints rather than forcing their unification. In this paper, we introduce nested sequent calculi for propositional standpoint logics--proof systems that manipulate trees whose nodes are multisets of formulae--and show how to automate standpoint reasoning by means of non-deterministic proof-search algorithms. To obtain worst-case complexity-optimal proof-search, we introduce a novel technique in the context of nested sequents, referred to as "coloring," which consists of taking a formula as input, guessing a certain coloring of its subformulae, and then running proof-search in a nested sequent calculus on the colored input. Our technique lets us decide the validity of standpoint formulae in CoNP since proof-search only produces a partial proof relative to each permitted coloring of the input. We show how all partial proofs can be fused together to construct a complete proof when the input is valid, and how certain partial proofs can be transformed into a counter-model when the input is invalid. These "certificates" (i.e. proofs and counter-models) serve as explanations of the (in)validity of the input.
