We introduce the flower calculus, a deep inference proof system for intuitionistic first-order logic inspired by Peirce's existential graphs. It works as a rewriting system over inductive objects called ''flowers'', that enjoy both a graphical interpretation as topological diagrams, and a textual presentation as nested sequents akin to coherent formulas. Importantly, the calculus dispenses completely with the traditional notion of symbolic connective, operating solely on nested flowers containing atomic predicates. We prove both the soundness of the full calculus and the completeness of an analytic fragment with respect to Kripke semantics. This provides to our knowledge the first analyticity result for a proof system based on existential graphs, adapting semantic cut-elimination techniques to a deep inference setting. Furthermore, the kernel of rules targetted by completeness is fully invertible, a desirable property for both automated and interactive proof search.

翻译：本文介绍花演算，一种受皮尔斯存在图启发的直觉主义一阶逻辑深层推理证明系统。该系统作为在称为“花”的归纳对象上的重写系统运作，这些对象既具有拓扑图形式的图形化解释，也具有类似于相干公式的嵌套序列的文本化表示。重要的是，该演算完全摒弃了传统的符号连接词概念，仅对包含原子谓词的嵌套花进行操作。我们证明了完整演算的可靠性以及一个分析片段相对于克里普克语义的完备性。据我们所知，这为基于存在图的证明系统提供了首个分析性结果，将语义切消技术适配于深层推理框架。此外，完备性所针对的核心规则集具有完全可逆性，这一性质对于自动与交互式证明搜索均具有重要价值。