amk*_*a00 5 formal-verification prolog logic-programming theorem-proving minikanren
我想在一些可能被称为完全声明的Horn逻辑(或完全声明的Prolog)中形式化一些知识并执行查询.任何人都可以提供一些如何实施它的指导方针吗？我简要回顾一下上面链接中的精细描述:
形式语言是Prolog的核心语言:"程序"是Prolog中的一组规则和事实(包括函数和变量,基本上只包含用户定义的谓词).
然而,与Prolog相比,我正在寻找一种完整的逻辑程序标准声明语义 - 最少Herbrand模型(即归纳定义的基础术语集).在逻辑编程的理论工作中,这通常是研究的对象,众所周知,可以获得对查询的完整和完整的答案(在"递归可枚举的"意义上),例如,使用SLD解析以下条件:
我正在寻找一个简洁的实现,它将建立在现有功能的基础上,而不是发明轮子.我看到的两个更有希望的方向是将它作为Prolog的元解释器实现,或者作为一些定理证明器的一部分.任何在这些领域具有实践知识的人都能提供一些如何实施它的指导方针吗？可以在miniKanren中轻松实现吗？
我的意图是以完全陈述的方式形式化一些知识.这种形式化的关键特征是它精确地对应于(单调)归纳的数学概念,因此可以通过归纳论证容易地推理知识及其属性.
在Prolog的几行中实现Horn逻辑的证明是一种简单的练习.从Vanilla Meta-interpreter开始,然后修改它以使用标准unify_with_occurs_check/2谓词进行所有统一,并使用完整的搜索过程 - 迭代深化第一次搜索是最简单的实现.
请参阅@ mat的页面Prolog中的一对Meta解释器获得一些灵感.