声明性的Horn逻辑？
我想将一些知识形式化，并在可能被称为完全陈述性的Horn逻辑（或者完全声明性的Prolog）中执行查询。 任何人都可以提供一些关于如何实现它的指导？ 我简要回顾一下上面链接的精细描述：
正式语言是Prolog的核心：“程序”是Prolog中的一组规则和事实（包括函数和变量，基本上只包含用户定义的谓词）。
然而，与Prolog不同的是，我正在寻找一种关于逻辑程序的标准声明性语义 - 最小Herbrand模型（即感应定义的基本术语集）的完善和完整的实现。 在逻辑编程的理论工作中，这通常是研究的对象，并且众所周知，对于查询的完整答案可以实现（以“递归可枚举”的意义），例如，使用SLD解析主题以下条件：
我正在寻找一个简明的实施方案，以现有能力为基础，而不是发明轮子。 我看到的两个更有希望的方向是将其作为Prolog的元解释器，或作为某个定理证明的一部分来实现。 任何具有这些领域实践知识的人都可以提供一些关于如何实施它的指南？ 它可以在miniKanren中轻松实现吗？
我的意图是以一种完全陈述的方式形式化一些知识。 这种形式化的关键特征在于，它恰好符合（单调）归纳的数学概念，因此知识和它的属性可以用归纳论证容易地推理。
在几行Prolog中实现Horn逻辑的证明者是一件容易的练习。 从Vanilla Meta解释器开始，然后修改它以对所有统一使用标准的unify_with_occurs_check/2谓词，并使用完整的搜索过程 - 迭代加深深度优先搜索是最简单的实现。
请参阅@ mat的页面一些灵感来自Prolog的元语言解释器。
更多的指针：
Datalog具有声明性语义，但作为“没有函数符号的Prolog”，它不是Prolog。 请参阅Ceri，Gottlob和Tanca出版的优秀介绍“你一直想知道关于Datalog（并且从未敢问）”。可通过CiteSeerX获得
Prolog的实现，使用制表符而不是深度优先搜索添加声明性（加上我了解的其他好的功能），如XSB。