一句话：提出守卫替换机制，在次原子逻辑中压缩证明，并可无需 cut 多项式模拟带替换的 Frege 系统。
次原子逻辑将原子视为二元连接词，使命题经典逻辑的证明系统具有严格线性推导：推理步骤不删除或添加信息。本文关注如何在此框架下压缩证明。作者提出守卫替换（guarded substitutions），一种显式替换变体，仅替换自由变量的受守卫出现而非全部出现，从而构造推导的“叠加”，同时表示多个子推导。主要结果表明，带守卫替换的次原子证明系统可以 p-模拟带替换的 Frege 系统，并且这一模拟不需要使用 cut 规则。
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.
@inproceedings{paperbot8630,
title = {Proof Compression via Subatomic Logic and Guarded Substitutions},
author = {Victoria Barrett and Alessio Guglielmi and Benjamin Ralph and Lutz Straßburger},
booktitle = {LICS},
year = {2025},
doi = {10.1109/lics65433.2025.00021}
}