田春冰河
2019-09-17 00:00:00 发布
[1/3] 没想到我刚刚完成 CCS 论文回到概率论形式化的课题上就取得小进展了。之前 HOL 里由于合并来自 HOL-Light 的代码导致有两个互相冲突的实数集下确界定义，必须把其中一个删除或转化成等价定理才能确保所有相关定理同时使用。这个问题我 2 月份的时候没能解决，但从 HOL 维护者那里得到了提示。