通过亚原子逻辑和受保护替换的证明压缩
Proof Compression via Subatomic Logic and Guarded Substitutions
AI总结：
本文提出受保护替换机制，用于亚原子逻辑中的证明压缩，通过仅替换自由变量的受保护出现来构造推导叠加，实现无需切割规则即可p-模拟带替换的Frege系统。
摘要：
亚原子逻辑是结构证明理论中的一项最新创新，其中原子不再被视为逻辑公式中的最小实体，而是被当作二元连接词来处理。因此，我们可以为命题经典逻辑给出一个亚原子证明系统，使得所有推导都是严格线性的：没有任何推理步骤删除或添加信息，甚至单位也是如此。在本文中，我们引入了一种强大的新证明压缩机制，称为受保护替换，它是显式替换的一种变体，仅替换自由变量的受保护出现，而非所有自由出现。这使我们能够构造推导的“叠加”，同时表示多个子推导。我们证明，带有受保护替换的亚原子证明系统可以p-模拟带有替换的Frege系统，而且，实现这一点不需要切割规则。
英文摘要：
Subatomic logic is a recent innovation in structural proof theory where atoms are no longer the smallest entity in a logical formula, but are instead treated as binary connectives. As a consequence, we can give a subatomic proof system for propositional classical logic such that all derivations are strictly linear: no inference step deletes or adds information, even units. In this paper, we introduce a powerful new proof compression mechanism that we call guarded substitutions, a variant of explicit substitutions, which substitute only guarded occurrences of a free variable, instead of all free occurrences. This allows us to construct ''superpositions'' of derivations, which simultaneously represent multiple subderivations. We show that a subatomic proof system with guarded substitution can p-simulate a Frege system with substitution, and moreover, the cut-rule is not required to do so.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
