文件名称：cheaplogic：基于分辨率的证明者找到所有证明
文件大小：443KB
文件格式：ZIP
更新时间：2024-03-13 00:26:09
resolution julia julia-language genie prover
cheaplogic（实验性） LogicalWorld命题逻辑系统。 我打算建立一个关于世界事实的查询-回答系统。 该系统是非常受限制的一阶。 关键概念：公理x模型矩阵，mgu向量是一个模型。 证明者基于解析原理的简单证明者。 旨在从给定公理中获得所有证明。 simpleprover在指定的搜索空间上运行。 但有时，它陷入无限循环，没有新的解决方案。 viewprover与用户具有GUI交互。 viewprover将Genie.jl用于Web界面。 从某种意义上说，它是一个证明者，它试图找到一个。 但这需要人类的帮助。 Prover / bterm / lisp /垃圾是对lisp的证明者的当前实现。