论文标题
与全直觉命题逻辑的应用以及应用的逻辑相关性搜索搜索两极分化的逻辑
Coinductive proof search for polarized logic with applications to full intuitionistic propositional logic
论文作者
论文摘要
本文扩展到了LJP，该方法被称为“共同证明搜索”，并由作者以前是由作者开发的，用于含义的直觉逻辑，该论文扩展到了LJP，这是一个集中的序列序列呈现极化直觉逻辑的序列呈现，包括一系列正面和负面连接。和以前一样，这包括对序列产生的搜索空间的共同感应描述，一个相同的感应语法描述了相同的空间，以及以递归语法上递归定义的谓词形式的居民问题的决策程序。我们通过这种递归程序证明了重点居民存在的可决定性，以及对极化直觉逻辑的重点居民数量的有限性。此外，两极分化的逻辑可以用作一个平台，从该平台中可以从中了解对其他逻辑的搜索。我们用LJT说明了该技术，LJT是一种集中的序列序列，用于完整的直觉命题逻辑（包括分离）。为此，我们必须确定LJT向LJP的“负翻译”（将所有直觉类型视为负类型），并验证翻译是否忠实地表示LJT中的证明搜索作为两极分化逻辑中的证明搜索。因此，我们继承了针对LJP研究的两个问题的可决定性，因此可以为LJT获得这些结果的新证明。
The approach to proof search dubbed "coinductive proof search", and previously developed by the authors for implicational intuitionistic logic, is in this paper extended to LJP, a focused sequent-calculus presentation of polarized intuitionistic logic, including an array of positive and negative connectives. As before, this includes developing a coinductive description of the search space generated by a sequent, an equivalent inductive syntax describing the same space, and decision procedures for inhabitation problems in the form of predicates defined by recursion on the inductive syntax. We prove the decidability of existence of focused inhabitants, and of finiteness of the number of focused inhabitants for polarized intuitionistic logic, by means of such recursive procedures. Moreover, the polarized logic can be used as a platform from which proof search for other logics is understood. We illustrate the technique with LJT, a focused sequent calculus for full intuitionistic propositional logic (including disjunction). For that, we have to work out the "negative translation" of LJT into LJP (that sees all intuitionistic types as negative types), and verify that the translation gives a faithful representation of proof search in LJT as proof search in the polarized logic. We therefore inherit decidability of both problems studied for LJP and thus get new proofs of these results for LJT.
