模态逻辑的前缀Tableau证明
Certification of Prefixed Tableau Proofs for Modal Logic
摘要：
不同的定理证明器倾向于以不同的格式产生证明对象，尤其是模态逻辑，其中已经提出了几种演绎形式主义（以及基于它们的证明器）。这项工作属于建立一个共同的规约语言，以证明在广泛的演绎形式主义的一般项目。特别是，通过使用从模态语言翻译成一阶极化语言和一个检查器，其小内核是基于一个经典的集中式微积分，我们能够证明模态证明标记的微积分，前缀tableaux和自由变量前缀tableaux。我们描述了逻辑K的一般方法，给出了它在一个类prolog语言中的实现，提供了一些例子，并讨论了如何将该方法扩展到其他正规模态逻辑
英文摘要：
Different theorem provers tend to produce proof objects in different formats and this is especially the case for modal logics, where several deductive formalisms (and provers based on them) have been presented. This work falls within the general project of establishing a common specification language in order to certify proofs given in a wide range of deductive formalisms. In particular, by using a translation from the modal language into a first-order polarized language and a checker whose small kernel is based on a classical focused sequent calculus, we are able to certify modal proofs given in labeled sequent calculi, prefixed tableaux and free-variable prefixed tableaux. We describe the general method for the logic K, present its implementation in a prolog-like language, provide some examples and discuss how to extend the approach to other normal modal logics
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
