双相似性下无1克莱尼星表达式的完备公理系统：一个初等证明
计算机科学中的逻辑
2021-11-23 v1
摘要
Grabmayer与Fokkink近期给出了二元克莱尼星下无1过程项在双相似等价下的有限完备公理化（LICS 2020会议论文集，预印本可得）。本文详述了一种不同且相当简洁得多的证明。该结果尽管仍有些技术化，但仅依赖于归纳法与范式，因此也更接近潜在的重写算法。此外，本文所有结果均提供了在Coq证明助手中的完备验证，但正确性并不依赖于任何计算机辅助方法。
引用
@article{arxiv.2111.11144,
title = {A Complete Axiom System for 1-Free Kleene Star Expressions under Bisimilarity: An Elementary Proof},
author = {Allan van Hulst},
journal= {arXiv preprint arXiv:2111.11144},
year = {2021}
}
备注
15 pages, for Coq-proofs contact the author