原子流深度推理中的规范化控制
Normalisation Control in Deep Inference via Atomic Flows
摘要：
我们引入“原子流”：它们是通过跟踪原子出现并忘记逻辑结构而从派生中获得的图。我们研究简单的操作原子流对应于复杂的减少派生。这使我们能够证明，命题逻辑，一个新的和非常普遍的规范化定理，其中包含削减消除作为一个特殊情况。我们在深度推理中操作，这比其他句法范式更普遍，并且规范化更难以控制。我们认为，原子流是规范化理论的一个重大技术进步，因为1）它们支持的技术在很大程度上独立于语法; 2）事实上，它在很大程度上独立于逻辑推理规则; 3）它们构成了一个强大的几何形式主义，比语法更直观。
英文摘要：
We introduce `atomic flows': they are graphs obtained from derivations by tracing atom occurrences and forgetting the logical structure. We study simple manipulations of atomic flows that correspond to complex reductions on derivations. This allows us to prove, for propositional logic, a new and very general normalisation theorem, which contains cut elimination as a special case. We operate in deep inference, which is more general than other syntactic paradigms, and where normalisation is more difficult to control. We argue that atomic flows are a significant technical advance for normalisation theory, because 1) the technique they support is largely independent of syntax; 2) indeed, it is largely independent of logical inference rules; 3) they constitute a powerful geometric formalism, which is more intuitive than syntax.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
