推理！-图
Reasoning with !-Graphs
摘要：
本论文的目的是提出一个扩展的字符串图的狄克逊，邓肯和基辛格，允许有限表示某些无限家庭的图形和图形重写规则，并证明了一个逻辑可以建立在此允许形式化的归纳证明在字符串图的紧凑封闭和跟踪对称monoidal类别。弦图提供了一种直观的方法来推理monoidal范畴。然而，这并不否定那些使用它们的人在证明中犯错误的能力。为此，有一个项目（Quantity）为字符串图构建了一个证明助手，至少对于那些基于具有跟踪概念的类别的字符串图。弦图的发展提供了弦图的组合形式化，为这个项目奠定了基础。交换Frobenius代数（CFA）在量子信息论中的流行，这些图的一个主要应用领域，已经导致使用变量节点作为Frobenius代数态射的归一化网络的简写，所谓的“蜘蛛记法”。这种符号极大地简化了CFA的推理，但是字符串图不足以正确地编码这种推理。本文扩展了字符串图，允许可变的节点表示，然后介绍！-盒符号（和结构来编码它）来表示包含重复子图的字符串图方程，其中重复的次数是任意的。然后，它演示了我们如何直接推理！图，被视为（通常是无限的）字符串图的家庭。特别值得注意的是一种基于图的归纳形式的呈现，允许对以前只能表示为字符串图和解释性文本的混合的证明进行正式编码。
英文摘要：
The aim of this thesis is to present an extension to the string graphs of Dixon, Duncan and Kissinger that allows the finite representation of certain infinite families of graphs and graph rewrite rules, and to demonstrate that a logic can be built on this to allow the formalisation of inductive proofs in the string diagrams of compact closed and traced symmetric monoidal categories. String diagrams provide an intuitive method for reasoning about monoidal categories. However, this does not negate the ability for those using them to make mistakes in proofs. To this end, there is a project (Quantomatic) to build a proof assistant for string diagrams, at least for those based on categories with a notion of trace. The development of string graphs has provided a combinatorial formalisation of string diagrams, laying the foundations for this project. The prevalence of commutative Frobenius algebras (CFAs) in quantum information theory, a major application area of these diagrams, has led to the use of variable-arity nodes as a shorthand for normalised networks of Frobenius algebra morphisms, so-called "spider notation". This notation greatly eases reasoning with CFAs, but string graphs are inadequate to properly encode this reasoning. This dissertation extends string graphs to allow for variable-arity nodes to be represented at all, and then introduces !-box notation (and structures to encode it) to represent string graph equations containing repeated subgraphs, where the number of repetitions is abitrary. It then demonstrates how we can reason directly about !-graphs, viewed as (typically infinite) families of string graphs. Of particular note is the presentation of a form of graph-based induction, allowing the formal encoding of proofs that previously could only be represented as a mix of string diagrams and explanatory text.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
