tableaux:用于公告逻辑的基于 Tableau 的定理证明器

公告逻辑的动态表 这个 Github 项目包含我在我的描述的公共公告逻辑的“动态”表系统的 Clojure 实现。 我简要地触及下面的一些关键词。 有关详细信息和文档，请参阅我的博士论文。 什么是公示逻辑？ 公告逻辑是对知识和公告进行推理的逻辑。 公告是一种学习形式，其中所有代理同时获得特定事实的共同知识。 什么是 tablau 系统？ Tableau 系统是用于构建满足给定公式的模型的正式系统。 它们也可用于在假设公式是定理的前提下证明定理，如果没有使用表格系统找到模型（这里就是这种情况）。 什么是动态画面？ 在我的论文中，我描述了各种动态模态逻辑的画面系统，包括公告逻辑。 这些画面系统具有密切反映动态模态逻辑的“动态”语义的规则。 使用说明 要开始，请执行以下步骤。 下载 。 请注意，安装 Java 运行时环境 (JRE) 可能还不够，因为它不会将命令行 Java 应用程序添加