BV 的证明同一性与范畴模型
计算机科学中的逻辑
2026-04-29 v1
摘要
BV-范畴是一项近期的发展，旨在为逻辑 BV 中的证明提供范畴语义。然而，由于一方面缺乏一致性定理，另一方面 BV 缺乏明确定义的证明同一性概念，BV-范畴与逻辑 BV 之间的精确关系仍不清楚。为了改善这一状况，我们在本文中基于原子流（可视为弦图的特殊形式）的概念，定义了 BV 的证明同一性概念。基于这一证明同一性概念，我们随后强化了现有的 BV-范畴概念，并证明其对逻辑 BV 是可靠的。
引用
@article{arxiv.2604.25501,
title = {Proof Identity and Categorical Models of BV},
author = {Matteo Acclavio and Lutz Straßburger and Vladimir Zamdzhiev},
journal= {arXiv preprint arXiv:2604.25501},
year = {2026}
}