HOL4中进程代数CCS的进一步形式化
计算机科学中的逻辑
2017-07-28 v2
摘要
在本项目中，我们扩展了先前关于在HOL4中形式化进程代数CCS的工作。我们添加了对弱互模拟等价和观察同余（根弱等价）的完全支持，包括相关定义、定理和代数律。一些深层引理也在本项目中得到形式化证明，包括邓引理（Deng Lemma）、Hennessy引理以及若干版本的“弱等价中包含的最粗同余”。对于最后一个定理，我们基于序数证明了完整版本（无任何假设）。
引用
@article{arxiv.1707.04894,
title = {Further Formalization of the Process Algebra CCS in HOL4},
author = {Chun Tian},
journal= {arXiv preprint arXiv:1707.04894},
year = {2017}
}
备注
24 pages with figures