证明助手中的共识动态逻辑
摘要：使用公共知识逻辑描述现实世界中涉及一组代理的情况。这些代理共享知识并对其他代理的知识提出强有力的陈述（即所谓的“共同知识”）。但是我们知道，现实世界是在变化的，关于世界的已知信息也会随之改变。这些变化由动态逻辑描述。为了描述知识的变化，动态逻辑应与公共知识逻辑相结合。本文描述了我们在证明辅助器Coq中进行的关于将公共知识逻辑和动态逻辑整合到一个统一框架中的实验。这导致了一组完全检查过的可读语句的证明。我们描述了该框架以及如何进行证明。
作者：Pierre Lescanne (LIP), J''er^ome Puiss''egur (LIP)
论文ID：0712.3146
分类：Computer Science and Game Theory
分类简称：cs.GT
提交时间：2007-12-20