一句话：提出直觉主义组合证明（ICPs），一种复杂度感知的几何语义，多项式保持序列演算翻译并实现局部典范性。
本文提出直觉主义组合证明（ICPs），为直觉主义逻辑给出一种具体的几何语义，推广自经典组合证明。每个 ICP 自然分解为线性片段（IMLL 证明网的图形抽象，即 arena net）与并行 contraction-weakening 片段（skew fibration）。ICP 与游戏语义关联，可视为 Hyland-Ong arena 中从树状推广到 DAG 状的策略。第一个主要结果是多项式完全性（Polynomial Full Completeness）：ICP 语义是复杂度感知的，其与序列演算之间的翻译可多项式大小保持；相比之下，lambda 演算与游戏语义会产生指数膨胀。第二个主要结果是局部典范性（Local Canonicity）：ICP 完全且忠实地抽象掉序列演算中非复制排列，类似作者对 MALL 的近期结果。该工作为直觉主义证明提供无语法、可组合的语义表示。
We present Intuitionistic Combinatorial Proofs (ICPs), a concrete geometric semantics of intuitionistic logic based on the principles of the second author's classical Combinatorial Proofs. An ICP naturally factorizes into a linear fragment, a graphical abstraction of an IMLL proof net (an arena net), and a parallel contraction-weakening fragment (a skew.fibration). ICPs relate to game semantics, and can be seen as a strategy in a Hyland-Ong arena, generalized from a tree-like to a dag-like strategy. Our first main result, Polynomial Full Completeness, is that ICPs as a semantics are complexity-aware: the translations to and from sequent calculus are size-preserving (up to a polynomial). By contrast, lambda-calculus and game semantics incur an exponential blowup. Our second main result, Local Canonicity, is that ICPs abstract fully and faithfully over the non-duplicating permutations of the sequent calculus, analogously to the first and second authors' recent result for MALL.