综合图论
Synthesising Graphical Theories
摘要：
近年来，图解语言已被证明是一个强大的和表达的工具，推理的物理，逻辑和语义过程表示为一个monoidal范畴中的态射。特别是，分类量子力学，或“量子图像主义”，旨在将量子理论的具体特征转化为抽象的结构属性，以图形恒等式的形式表达。我们搜索这些属性的一种方法是从一个具体的模型（例如一组线性映射或有限关系）开始，并开始将生成器组成图并寻找图形标识。简单地说，我们可以通过枚举给定大小的所有图并检查等式来自动化这个过程，但这在实践中很难处理，因为它产生了太多的等式。幸运的是，这些恒等式中有许多不是原始的，而是可以从更简单的恒等式推导出来的。2010年，Johansson、Dixon和Bundy开发了一种称为猜想合成的技术，用于自动生成约束项方程，以输入到归纳定理证明器中。在这个扩展的摘要中，我们将这种技术应用于图形理论，表示为图形重写系统，并通过合成用于研究纠缠量子态的图形理论来演示其应用。
英文摘要：
In recent years, diagrammatic languages have been shown to be a powerful and expressive tool for reasoning about physical, logical, and semantic processes represented as morphisms in a monoidal category. In particular, categorical quantum mechanics, or "Quantum Picturalism", aims to turn concrete features of quantum theory into abstract structural properties, expressed in the form of diagrammatic identities. One way we search for these properties is to start with a concrete model (e.g. a set of linear maps or finite relations) and start composing generators into diagrams and looking for graphical identities. Naively, we could automate this procedure by enumerating all diagrams up to a given size and check for equalities, but this is intractable in practice because it produces far too many equations. Luckily, many of these identities are not primitive, but rather derivable from simpler ones. In 2010, Johansson, Dixon, and Bundy developed a technique called conjecture synthesis for automatically generating conjectured term equations to feed into an inductive theorem prover. In this extended abstract, we adapt this technique to diagrammatic theories, expressed as graph rewrite systems, and demonstrate its application by synthesising a graphical theory for studying entangled quantum states.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
