面向基于术语的图谱等价验证的探索
计算机科学中的逻辑
2026-02-12 v1
摘要
字符串图是一种二维图表示，可描述为由基本单元通过顺序与并行组合生成的一维术语。由于不同的语法术语可能表示相同的图谱，该语法被经济方程组所商quo，这些方程表达关于变形的等价性。本工作为自动化推理图谱等价性奠定了基础，主要动机是验证量子电路的等价性。我们考虑两类图谱，针对这两类图谱引入归一化术语重写系统，以等价图谱等价的术语。我们在两者之间证明了终止性与一致性，借助 Isabelle/HOL 证明助手完成。
关键词
引用
@article{arxiv.2602.11035,
title = {Towards Term-based Verification of Diagrammatic Equivalence},
author = {Julie Cailler and Noé Delorme and Simon Perdrix and Sophie Tourret},
journal= {arXiv preprint arXiv:2602.11035},
year = {2026}
}