一句话：揭示一阶逻辑组合证明与句法证明的关系，通过深度推理分解定理给出新正规形式及可靠/完备/完全完备性结果。
本文研究一阶逻辑（不含等词）中组合证明与句法证明之间的深层联系。句法证明由推理规则形式化，组合证明则是无语法、独立于推理规则集合的证明呈现。作者通过深度推理分解定理将两者联系起来，并为句法证明建立了一种新的正规形式。基于该定理，作者给出组合证明可靠性与完备性的简洁证明，表明其与一阶逻辑有效性一致；同时证明完全完备性：每个组合证明都是某个句法证明的像，说明组合证明未超出句法证明的表达范围。该工作为组合证明提供了句法基础，并深化了对一阶逻辑证明结构与正规形式的理解。
We uncover a close relationship between combinatorial and syntactic proofs for first-order logic (without equality). Whereas syntactic proofs are formalized in a deductive proof system based on inference rules, a combinatorial proof is a syntax-free presentation of a proof that is independent from any set of inference rules. We show that the two proof representations are related via a deep inference decomposition theorem that establishes a new kind of normal form for syntactic proofs. This yields (a) a simple proof of soundness and completeness for first-order combinatorial proofs, and (b) a full completeness theorem: every combinatorial proof is the image of a syntactic proof.