A Subatomic Proof System for Decision Trees
A Subatomic Proof System for Decision Trees
复制标题
决策树的亚原子证明系统
DOI：
10.1145/3545116
复制
发表时间：
2022
影响因子：
0.5
通讯作者：
Barrett C
中科院分区：
文献类型：
--
作者：
Barrett C
我们设计了一个命题经典逻辑的证明系统，它集成了布尔函数的两种语言：标准合取-析取-否定和二叉决策树。我们有两个理由这样做。第一个是证明-理论自然性：该系统由所有且仅由最近引入的亚原子逻辑的单一、简单、线性方案生成的推理规则组成。由于这种规律性，通过自然结构消除了切割。第二个原因是该系统产生了高效的证明。事实上，我们证明了一类由Statman引起的重言式在我们的系统中具有多项式的无切割证明，它们在序演学中不能有比指数更好的无切割证明。我们通过使用与削减相同的结构来实现这一目标。综上所述，通过扩展命题逻辑的语言，我们使命题逻辑的证明理论更加规则，生成了更多的证明，其中一些证明是非常有效的。这种设计是通过将原子视为它们真值的叠加而实现的，这些真值是通过自对偶、非交换连接词连接起来的。然后，一个证明可以通过每个原子投射成两个证明，每个证明对应一个真值，而不需要切割。这些投影在语义上是自然的，是本文结构的核心。为了适应自对偶非交换性，我们在深度推理中构造了证明。
We design a proof system for propositional classical logic that integrates two languages for Boolean functions: standard conjunction-disjunction-negation and binary decision trees. We give two reasons to do so. The first is proof-theoretical naturalness: The system consists of all and only the inference rules generated by the single, simple, linear scheme of the recently introduced subatomic logic. Thanks to this regularity, cuts are eliminated via a natural construction. The second reason is that the system generates efficient proofs. Indeed, we show that a certain class of tautologies due to Statman, which cannot have better than exponential cut-free proofs in the sequent calculus, have polynomial cut-free proofs in our system. We achieve this by using the same construction that we use for cut elimination. In summary, by expanding the language of propositional logic, we make its proof theory more regular and generate more proofs, some of which are very efficient.That design is made possible by considering atoms as superpositions of their truth values, which are connected by self-dual, non-commutative connectives. A proof can then be projected via each atom into two proofs, one for each truth value, without a need for cuts. Those projections are semantically natural and are at the heart of the constructions in this article. To accommodate self-dual non-commutativity, we compose proofs in deep inference.
登录
查看更多内容
相互作用和结构的系统
DOI：
--
发表时间：
1999
期刊：
TOCL
影响因子：
--
作者：
Alessio Guglielmi
通讯作者：
Alessio Guglielmi
经典谓词逻辑的深度推理系统中的剪切消除
影响因子：
0.7
作者：
Kai Brünnler
通讯作者：
Kai Brünnler
谓词演算中证明搜索和加速的界限
DOI：
--
发表时间：
1978
期刊：
影响因子：
--
作者：
R. Statman
通讯作者：
R. Statman
亚原子证明系统
DOI：
10.1145/3173544
发表时间：
2017
期刊：
ACM Transactions on Computational Logic (TOCL)
影响因子：
--
作者：
Andrea Aler Tubella;Alessio Guglielmi
通讯作者：
Alessio Guglielmi
经典逻辑的局部系统
DOI：
10.1007/3-540-45653-8_24
发表时间：
2001
期刊：
Log. Methods Comput. Sci.
影响因子：
--
作者：
Kai Brünnler;Alwen Tiu
通讯作者：
Alwen Tiu