文件名称：flp:FLP不可能定理的形式化
文件大小：6KB
文件格式：ZIP
更新时间：2024-05-26 17:37:53
Coq
使用Coq交互式定理证明器对FLP不可能定理进行形式化 模型是仿照。 其他建设性证明： : 10.1.1.221.7907& rep1&type= ， : ，但这是第一个公开源代码！ lemma3的证明也不同于以前的所有证明。 纸快来了！ 希望将其发表在同行评审的期刊上。 ##模型与公理 消息完全被跳过了（因此仅出于更好的理解而需要它们，而为了证明起见，我们只能讨论系统的状态转换）。 Process是原始文件中的自动机。 就我们的目的而言，枚举具有一些自然数的状态，并在数字中也编码过程标识符就足够了，因此存在双向注入式映射（process_id，state）<-> nat。 Definition Process := nat. 那么配置只是进程列表： Definition Configuration := list Process. 事件也用自然数枚举，具有
【文件预览】：
flp-master
----flp.v(13KB)
----README.md(4KB)
----.gitignore(8B)