A Diagrammatic Axiomatisation for Qubit Entanglement
关于么半群范畴的推理的图解技术提供了对相互作用的计算过程的对称性和连接的直观理解。在分类量子力学的背景下，Coecke和Kissinger建议两个3-qubit态GHZ和W可以用作新的图形演算的构建块，旨在对多体量子比特纠缠进行图形分类，突出量子态的通信特性及其在加密方案中的潜在用途。在本文中，我们提出了一个完整的图形公理化GHZ和W之间的关系：ZW演算。这改进了先前存在的ZX演算的一个版本，同时保持了它最令人满意的特性：无向性、高度对称性和代数基础。我们证明了ZW演算是完整的自由阿贝尔群的两个发电机的幂的类别-“整数系数的量子比特”-并提供了一个明确的规范化过程。
2015-01-28 cs.LO math.CT quant-ph
AC Simplifications and Closure Redundancies in the Superposition Calculus
结合性和交换性（AC）的存在下的推理是众所周知的挑战，由于这些公理的多产性。AC公理的专业化处理主要是由基于Knuth-Benzynn完备的单位等式证明器支持的。在这些验证器中处理AC的主要成分是适用于AC的地面可连接性标准。本文将AC可连接性从单位等式和Knuth-Beneficiary完备化推广到叠加演算和全一阶逻辑。我们的方法是基于扩展的Bachmair-Ganzinger模型建设和一个新的冗余标准，其中包括地面可连接性。我们的方法的一个副产品是一个新的标准，适用性的解调，我们称之为解调器解调。这个标准是有用的，在任何叠加定理证明，独立的AC理论，我们证明，它使解调在更多的情况下，相比标准标准。
2021-07-18 cs.LO
ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification
本文提出了一种新的算法方法进行自动化的图形演绎组合结构，使用修改后的方程定理证明技术和扩展的Wolfram模型超图重写形式主义的作者在以前的工作。我们特别关注这种新算法在量子信息论中的自动电路简化问题上的应用，使用Wolfram模型多路算子系统与ZX演算形式主义相结合，在量子比特之间的线性变换上进行快速图解推理。我们将展示如何构建一个推广的演绎推理规则的克努特-Benjunt完成方程匹配的基础上选择的因果边缘密度在相关的多路系统，然后再演示如何嵌入高阶逻辑的ZX演算规则在这个一阶方程框架。在明确展示了Wolfram模型系统和ZX演算的（超）图重写如何在这种形式主义中有效地实现之后，我们继续展示这种新算法方法的时间复杂度与证明复杂度的比较，当将随机生成的Clifford电路简化为伪范式时，以及当减少随机生成的非Clifford电路中的T门数量时，电路尺寸范围高达3000门，说明该方法与现有的电路简化框架相比表现良好，并且还表现出通过采用因果边密度优化获得的近似二次加速比。最后，我们提出了一个简单的量子隐形传态协议的正确性自动证明的工作实例，以更清楚地展示定理证明过程的内部操作。
2021-03-29 cs.DM cs.LO
Completeness of Synthesis under Realizability Assumptions using Superposition
TU Wien（维也纳工业大学）
本文研究了在可实现性假设下利用超位置进行程序合成的完备性问题，通过改进超位置演算并证明其正确性和完备性，确保能够找到满足规范的可计算程序。
2026-05-19 cs.LO
A Superposition Calculus for Abductive Reasoning
Univ. Grenoble Alpes（格勒诺布尔阿尔卑斯大学）；CNRS（法国国家科学研究中心）；LIG（格勒诺布尔信息学实验室）
我们提出了一个修改的叠加演算是为了产生的一阶公理集的后果。这种方法被证明是健全的和演绎完整的冗余消除规则的存在下，所考虑的后果是建立在一个给定的有限的地面条款，由常数符号表示。与其他方法相比，大多数关于叠加演算终止的现有结果可以结转到我们的程序中。这特别确保了对于SMT社区感兴趣的许多理论来说，微积分是终止的。
2014-07-13 cs.AI cs.LO
Hierarchic Superposition Revisited
自动演绎的许多应用需要在一阶逻辑模背景理论中进行推理，特别是某种形式的整数运算。一个主要的未解决的研究挑战是设计定理证明器，即使在存在自由函数符号的情况下也是“合理完整的”，这些符号范围为背景理论排序。Bachmair，Ganzinger和Waldmann的层次叠加演算已经支持这样的符号，但是，正如我们所证明的，不是最优的。本文旨在通过引入一种新的子句抽象形式来纠正这种情况，这是分层叠加演算中的核心组件，用于将子句转换为内部操作所需的形式。我们认为所产生的演算的好处，并提供两个新的完整性结果：一个片段，所有背景排序的条款是地面和另一个特殊情况下的线性（整数或理性）算术作为背景理论。
2019-04-17 cs.LO
ZX-Calculus and Extended Hypergraph Rewriting Systems I: A Multiway Approach to Categorical Quantum Information Theory
范畴量子力学和Wolfram模型提供了不同但互补的方法来研究组合结构上的图形重写系统与物理学基础之间的关系;本文的目的是在Coecke和Duncan的ZX演算形式主义的背景下开始阐明这两种方法之间的形式对应关系，用于图解地推理量子比特之间的线性映射。在简要总结了相关的形式主义，并提出了一个明确的公式的Wolfram模型的粘合剂类别和双推出重写系统，我们说明了如何图形重写的ZX演算可以嵌入和实现在更广泛的背景下Wolfram模型多路系统，并举例说明我们专门为此目的开发的软件框架（ZXMultiwaySystem）的一些功能。最后，我们提出了一个证明（连同一个明确计算的例子）的方法的基础上的狄克逊和基辛格的多路演化图和分支图的Wolfram模型是自然赋予monoidal结构的基础上rulial组成，而且，兼容的monoidal产品的ZX图。
2020-10-05 cs.DM cs.LO
Optimistic Higher-Order Superposition
Max Planck Institute for Informatics, Campus E1 4, 66123 Saarbrücken, Germany（马克斯·普朗克信息研究所）
本文提出“乐观”版$λ$-superposition演算，通过子句约束延迟爆炸性合一问题并定向应用函数外延性，在保持Henkin语义下可靠且反驳完备的同时提升证明效率。
2025-10-21 cs.AI cs.LO
Relational Diagrams: a pattern-preserving diagrammatic representation of non-disjunctive Relational Queries
通过关系语言的逻辑表达能力来分析关系语言是很容易理解的。关系查询模式的模糊概念还没有得到很好的理解，甚至还没有正式化。什么是查询模式？我们如何在不同的关系语言中推理查询模式，而不管它们的语法和它们的过程性或声明性？在本文中，我们形式化的概念，查询模式的关系原子之间的模式保持映射的变体。这种形式主义使我们能够分析关系查询语言的相对模式表达能力，并创建一个层次结构的语言具有相同的逻辑表达能力，但不同的模式表达能力。在这种分析中，关系演算可以表达比关系代数的基本运算符更多的模式。我们还贡献了一个直观的，完整的，和声音的图形表示安全的关系演算，不仅是关系完整的，但也可以表达所有的逻辑模式的大型和有用的片段的非析取关系演算。在我们所知道的所有关系查询的图形表示中，这是唯一一个关系完整的，可以表示非析取片段中的所有逻辑模式。
2022-03-14 cs.DB cs.LO cs.PL
Quantum Machine Learning using the ZXW-Calculus
量子机器学习（QML）领域探索如何使用量子计算机更有效地解决机器学习问题。作为量子-经典混合算法的一种应用，它在近期内有望发挥潜在的量子优势。在这篇论文中，我们使用ZXW演算来图解分析QML应用所面临的两个关键问题。首先，我们讨论在量子硬件上计算梯度的算法，这些算法是为QML执行基于梯度的优化所需的。具体地说，我们给出了新的图解证明，在文献中使用的常见的2和4项参数移位规则。此外，我们推导出一种新的，广义的参数移位规则与2n项，适用于门，可以表示与n参数化蜘蛛在ZXW演算。此外，据我们所知，我们给出了Anselmetti等人的一个猜想的第一个证明。通过证明一个不可行定理，排除了4项移位规则的更有效的替代方案。其次，我们分析了贫瘠高原的量子ansätze的梯度景观，使用经验和分析技术。具体地说，我们开发了一个工具，可以自动计算梯度的方差，并使用它来检测常用量子ansätze中可能的贫瘠高原。此外，我们正式证明存在或不存在的贫瘠高原的选择ansätze使用图表技术从ZXW演算。
2022-10-18 cs.LO quant-ph
Superposition for Fixed Domains
Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）
叠加是一个既定的决策过程，为各种一阶逻辑理论表示的条款集。一个可满足的理论，饱和叠加，隐含地定义了一个最小项生成的模型的理论。证明关于饱和理论的普适性质直接导致最小模型的项生成域的修改，因为引入了新的Skolem函数。对于许多应用，这是不期望的。因此，我们提出了第一个叠加演算，可以明确表示存在量化的变量，从而可以计算相对于一个给定的域。这种演算是健全的和反驳完全的限制一阶固定域语义。对于饱和Horn理论和正公式类，我们甚至可以使用微积分来证明最小模型本身的性质，超出了已知的基于叠加的方法的范围。
2009-11-30 cs.AI cs.LO
Superposition with Lambdas
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）；Max-Planck-Institut für Informatik（马克斯·普朗克信息学研究所）
我们设计了一个叠加演算的延伸多态高阶逻辑，包括匿名函数，但不包括布尔的子句片段。推理规则作用于$λ$-项的$βη$-等价类，并依赖于高阶统一来实现反驳完备性。我们在Zipperposition证明器中实现了微积分，并在TPTP和Isabelle基准测试中进行了评估。结果表明，叠加是一个合适的基础高阶推理。
2021-01-31 cs.AI cs.LO
Superposition with Delayed Unification
University of Manchester（曼彻斯特大学）；TU Wien（维也纳技术大学）
该研究将合一操作从原子步骤提升到演算层面，把合一算法步骤转化为推理步骤，证明了一阶叠加演算在这种延迟合一机制下仍保持完备性，讨论了其对标准一阶叠加的优势并给出实验评估，为依赖大量/无限合一符的演算提供了合一与推理交错的新思路。
2024-02-29 cs.AI cs.LO
Term Orders for Optimistic Lambda-Superposition
针对 λ-超叠加演算的项序需求，提出 $λ$KBO 与 $λ$LPO，并借助到一阶 KBO/LPO 的编码证明其具备所需性质。
2025-10-21 cs.LO
SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning
Max Planck Institute for Informatics（马克斯·普朗克信息学研究所）；Graduate School of Computer Science（计算机科学研究生院）
本文证明了 SCL(FOL) 能通过特定策略模拟 Superposition 在无等式一阶逻辑中的非冗余子句推导，表明 SCL 演算是 Superposition 演算的推广。
2023-05-22 cs.AI cs.LO cs.SC
Interacting Quantum Observables: Categorical Algebra and Diagrammatics
本文有两个紧密交织的目标：（i）介绍一种直观和通用的多量子比特系统的图形演算，ZX演算，它大大简化了量子计算和信息领域的推导。(ii)公理化量子观测量的互补性，在一个一般的框架内的物理理论的匕首对称幺半群范畴。我们还公理化在这个框架内的相移。使用良好的研究规范之间的对应关系的图形演算和对称monoidal类别，我们的研究结果提供了一个纯粹的图形形式化的互补量子观测。每一个单独的可观测量，由一个交换的特殊匕首弗罗贝纽斯代数表示，产生一个阿贝尔群的相移，我们称之为相位群。我们还确定了一个强大的形式的互补性，满足Z和X自旋观测量，从而产生一个缩放的双代数的变体。
2011-04-21 cs.LO math.CT math.QA
Three qubit entanglement within graphical Z/X-calculus
应用范畴量子力学的合成技术分析了3比特量子纠缠。特别是由于邓肯和作者之一的互补可观测量和相应的相位的图形演算被用来构建两个真正的三方SLOCC类的3-qubit纠缠态，GHZ和W的代表成员。这很好地说明了在W-和GHZ-类态中分别发现的成对和全局三重纠缠。一个新的概念的concernentarity允许我们在抽象的图解演算中的居民的W类;这些方法扩展到更一般的多体量子比特状态。
2011-03-14 cs.LO quant-ph
Two linearities for quantum computing in the lambda calculus
我们提出了一种方法来统一量子代数演算中的两种非克隆方法：逻辑线性和代数线性。第一种方法是禁止重复变量，而第二种方法是将所有的非线性项都视为代数线性函数。我们通过定义一阶简单类型的量子扩展来说明这个想法，其中类型在叠加上是线性的，同时允许克隆基向量。此外，我们提供了一个解释的演算叠加类型被解释为向量空间和非叠加类型作为其基础。
2019-07-31 cs.LO
The decohered ZX-calculus
本文通过退相干ZX演算的生成元，提出一个通用且完备的演算片段，用于仿射支撑概率分布，并给出范式，为处理混合经典-量子过程及更一般概率过程奠定基础。
2025-08-06 cs.LO quant-ph
A Comprehensive Tutorial on over 100 Years of Diagrammatic Representations of Logical Statements and Relational Queries
本教程系统梳理了逾百年来逻辑语句与关系查询的图形化表示方法，通过将视觉隐喻映射到关系代数和关系演算，帮助用户理解复杂查询。
2024-03-05 cs.DB cs.LO
Equational Theorem Proving for Clauses over Strings
本文针对字符串上一般子句的等式推理研究不足问题，提出一种新的带字符串的叠加演算及定理证明框架，证明其反驳完全性，并给出基于有限饱和的字符串字问题判定过程。
2023-03-23 cs.LO
A Process Calculus for Molecular Interaction Maps
我们提出了MIM演算，一个强大的生物基础的建模形式主义，它提供了生物意义的运营商代表的分子物种的相互作用能力。微积分的运算符受到分子相互作用图（MIM）中使用的反应符号的启发，MIM是生物学家使用的一种图形符号。模型的演算可以很容易地从MIM图，从而获得一个明确的和可执行的解释。我们给出了MIM演算的语法和语义的形式化定义，并研究了形式化的性质。一个案例研究也显示使用的演算建模生物分子网络。
2009-11-25 cs.CE cs.LO q-bio.MN
Graphical Algebraic Geometry: From Ideals and Varieties to Quantum Calculi
University of Oxford（牛津大学）
本文提出图示代数几何（GAG），扩展了图示线性代数程序，证明其在代数结构的（co）span语义下是通用且完整的，展示了GAG在多项式约束网络中的重写系统应用及对量子计算中qudit ZH算子的扩展。
2026-05-13 cs.LO math.CT quant-ph
Scroll nets
我们介绍了一种新的形式主义命题逻辑中的证明称为“涡卷网”。它的基本结构是C. S.皮尔士在19世纪末作为他的存在图（EGs）图解系统的基础。涡卷网是通过遵循Curry-Howard方法将推理规则内在化到判断中而从EGs衍生出来的，就像类型论中的术语将自然演绎规则内在化一样。我们专注于EGs的直觉暗示片段，从一个自然的图形表示的涡卷网，然后提取其组合的本质到一个纯粹的图论定义。我们还确定了绕道的概念，我们用它来勾画一个绕道消除过程类似于削减消除。我们说明了如何模拟规范化的简单类型的$λ$演算，演示了我们的框架的逻辑和计算的表达能力。
2025-07-25 cs.LO
ZX-Calculus: Cyclotomic Supplementarity and Incompleteness for Clifford+T quantum mechanics
ZX演算是量子力学和量子信息处理的一种强大的图形语言。语言的完整性--即导出任何真实方程的能力--是一个至关重要的问题。在寻求完整的ZX演算时，最近已经证明了平行性对于量子图推理是必要的（MFCS 2016）。粗略地说，平行性包括合并两个子图时，他们被参数化的对跖角。我们介绍了一个广义的cyclo-tomic cycloentarity-它包括在合并n个子图一次，当n个角度划分成相等的部分圆。我们证明了当n是奇素数时，分圆连续性是不能导出的，从而为图解量子推理提供了一个可数的新公理族，我们展示了另一个不能从ZX演算的现有规则导出的新的简单公理，特别是暗示了Clifford+T量子力学语言的不完备性.我们最终得到了一个新的公理化的扩展ZX-演算，包括一个公理模式的分圆的concurrentarity。
2017-06-26 cs.LO quant-ph
Towards a Computational Quantum Logic: An Overview of an Ongoing Research Program
本文概述了将Curry-Howard-Lambek对应扩展至量子计算的研究计划，通过提出Lambda-$S$演算和$\mathcal L^{\mathbb C}$演算两个框架，为量子编程语言建立逻辑与计算基础，揭示了量子计算与线性逻辑间的对偶性。
2025-04-10 cs.LO
Rewriting and Inductive Reasoning
针对传统重写在归纳推理中遗漏关键后承的问题，本文扩展 superposition 演算以在饱和中自动生成充分后承，并在 Vampire 上验证其单元等式归纳推理性能显著提升。
2024-02-29 cs.LO
The ZX calculus is a language for surface code lattice surgery
用于可扩展量子计算的纠错的主要选择是具有晶格手术的表面码。基本的晶格手术操作，逻辑量子比特的合并和分裂，对逻辑状态起非幺正作用，并且不容易被标准电路符号捕获。这就提出了如何最好地设计、验证和优化使用网格手术的协议的问题，特别是在具有复杂资源管理问题的架构中。在本文中，我们证明了操作的ZX演算-一种形式的量子图形推理的基础上双代数-完全匹配的操作格手术。红色和绿色的“蜘蛛”节点匹配粗糙和光滑的合并和分裂，并遵循匕首特殊关联Frobenius代数的公理。一些格外科手术操作需要非平凡的校正操作，其在使用ZX演算时以图的集合的形式原生地捕获。我们给出了第一次尝试的权力的演算作为一种语言的晶格手术考虑两个操作（T门和生产CNOT），并显示如何ZX图重写规则给晶格手术程序，这些操作是新颖的，高效的，高度可配置的。
2020-06-04 cs.LO quant-ph
Enriching Diagrams with Algebraic Operations
本研究通过单子的Eilenberg-Moore代数范畴富集幺半范畴，构造伴随函子，拓展带概率选择的ZX-calculus及其语义，可用于量子系统噪声的图推理。
2024-01-29 cs.LO quant-ph
Premonoidal Semantics and Scalable Diagrammatics of Fermionic Quantum Computing
Inria（法国国家信息与自动化研究所）；LIX, École Polytechnique（巴黎综合理工学院LIX实验室）；CPHT, CNRS（法国国家科学研究中心CPHT中心）；Institut Polytechnique de Paris（巴黎理工学院）
本文针对费米子量子计算中并行组合交换律失效的问题，提出对称预幺半范畴语义，并引入pronaps扩展图解记号，为费米子ZW演算的多个片段给出规范形式和完备性证明，连接了电路语义、图解重写与行列式代数。
2026-10-05 cs.LO quant-ph
Fast Automated Reasoning over String Diagrams using Multiway Causal Structure
我们介绍了一个直观的算法方法，用于在一般的双推出（DPO）框架内执行自动重写字符串图，其中重写的顺序是根据底层图解演算的因果结构来选择的。重写结构和因果结构的组合可以被优雅地表述为一个弱2-范畴，配备了全部和部分monoidal双函子，从而为通用Wolfram模型超图重写系统的全多向进化因果图提供了范畴语义。作为一个说明性的例子，我们展示了这种算法的一个特殊情况下如何实现高效的自动化简化量子电路，如ZX演算所示。
2021-05-10 cs.DM cs.LO
The Many-Worlds Calculus
本研究探讨乘法与加法两种幺半结构的相互作用，提出着色PROP建模带代数副作用参数化选择的计算，构建带线性指称语义与等式理论的图形语言，证明其通用性与等式理论的完备性，可支持正则、概率、非确定及量子分支计算。
2025-05-15 cs.LO quant-ph
Completeness of the ZX-Calculus
本文通过添加公理并利用第三方图形化语言的来回翻译，证明了ZX-演算在克利福德+T片段及整体上的完备性，并扩展至线性图类，最后为含额外生成器的简化版本给出完备公理化。
2020-06-03 cs.LO quant-ph
Complete equational theories for classical and quantum Gaussian relations
该研究给出经典与量子高斯关系的超图道具等式表示，扩展了相关理论与图形演算，为量子光学的非正式计算提供严格依据并支持多种光学操作推理。
2024-04-10 cs.LO math.CT quant-ph
A concrete model for a typed linear algebraic lambda calculus
本文为带测量的类型化线性代数 lambda 演算 Lambda-S 构造了基于集合与复向量空间范畴伴随关系的具体模型，用隐藏的遗忘函子解释叠加类型 S。
2023-10-11 cs.LO math.LO
Strong Complementarity and Non-locality in Categorical Quantum Mechanics
范畴量子力学在匕首紧闭范畴的框架下研究量子理论。使用这个框架，我们建立了两个关键的量子理论概念之间的紧密关系：非局部性和互补性。特别是，我们建立了Mermin型非局部性的情况下，我们推广到任意数量的缔约方，使用系统的任意尺寸，并执行任意测量，和一个新的更强的互补性的概念，我们在这里介绍之间的直接连接。我们推导的事实，强互补性是一个必要条件的Mermin方案提供了一个清晰的操作解释强互补性。我们还提供了一个完整的分类强互补观测的量子理论，这还没有实现普通的互补。由于我们的主要结果是用匕首紧范畴的（图解）语言表达的，它们可以应用于量子理论之外，任何支持强互补观测量的纯代数概念的环境中。因此，除了量子理论之外，我们还介绍了一种在各种各样的模型中讨论非定域性的方法。图解演算大大简化了（有时甚至是琐碎化了）许多推导，并提供了新的见解。特别是，相关性的图解计算清楚地显示了局部测量如何相互作用以产生全局整体效应。换句话说，我们描述了非定域性。
2012-04-27 cs.LO math.CT quant-ph
Picturing classical and quantum Bayesian inference
我们介绍了一个图形框架贝叶斯推断，是足够普遍的，以适应不仅是标准的情况下，但最近的建议，量子贝叶斯推断的理论，其中一个认为密度算子，而不是概率分布的代表程度的信念。图解框架是在对称monoidal范畴的图形语言和紧凑的结构和Frobenius结构，其中贝叶斯反演归结为一个适当的紧凑结构的换位。我们表征经典的贝叶斯推断的图形属性，并表明，我们的方法消除了一些纯粹的传统元素，出现在其共同的表示，如是否程度的信念表示的概率或熵量。我们还介绍了一个量子演算，其中的Frobenius结构是非交换的，并表明它可以容纳Leifer的演算的“条件密度算子”。条件独立的概念也推广到我们的图形设置，我们做了一些初步的贝叶斯网络理论的连接。最后，我们演示了如何构建一个图形贝叶斯演算内的任何匕首紧凑的范畴。
2011-02-11 cs.LO math.CT math.PR
A New Algorithmic Decision for Categorical Syllogisms via Caroll's Diagrams
Ege University（埃格大学）
本文讨论了一个演算系统SLCD（SyllogisticLogicwithCarrollDiagrams），它给出了用图进行逻辑推理的一种形式化方法，它表示了基本的阿伦特范畴命题，并证明了它们在删除中间项的三段论推理准则下是封闭的。因此，它的实施，让形式主义包括同步双边和三边的数学外观和一个天真的算法性质。而且，不需要专门的知识或专门的能力来理解和使用它，因此，我们给出了一个有效的算法，用于确定是否有效的三段论推理使用SLCD。
2021-01-28 cs.AI cs.LO
Infrared Safety from ZX-Diagrams: A Categorical Proof of Soft-QED as Open Quantum System
Kwangwoon University（光云大学）
利用丢弃ZX演算给出QED红外发散的Bloch-Nordsieck抵消的非微扰范畴证明，将软光子视为开放量子系统的环境，通过图论恒等式验证了软光子定理和退相干效应。
2026-06-29 cs.LO hep-th math-ph
