如何实现完全声明式角逻辑？

Question

我想将一些知识正规化，并在所谓的完全声明式喇叭逻辑 (或完全声明式Prolog)中执行查询。有人能提供一些关于如何实施它的指导方针吗？我简单地回顾一下上面的链接中的详细描述：

形式语言是Prolog的核心：“程序”是一组规则和事实，就像Prolog中的那样(包括函数和变量，基本上只包含用户定义的谓词)。

然而，与Prolog不同的是，我正在寻找一个与逻辑程序的标准声明性语义有关的合理和完整的实现--最小的Herbrand模型(即归纳定义的一组地面术语)。在逻辑编程的理论工作中，这通常是研究的对象，众所周知，可以获得对查询的合理和完整的答案(在“递归-枚举”的意义上)，例如，使用SLD分辨率，但需满足以下条件：

• 搜索匹配规则(例如，Prolog的深度优先搜索是而不是公平)；
• 与"occurs-check“统一(检查变量是否在与其统一的术语中出现)。

我正在寻找一个简洁的实现，它将建立在现有功能的基础上，而不是发明轮子。我看到的两个更有希望的方向是将其实现为Prolog的元解释器，或者作为某个定理证明器的一部分。在这些领域有实际知识的人能就如何实现它提供一些指导吗？它能在miniKanren中容易地实现吗？

我的意图是以一种完全声明的方式将一些知识正规化.这种形式化的关键特征是它与(单调)归纳的数学概念完全相对应，从而使知识及其性质可以很容易地用归纳论证来解释。

Answer 1

在Prolog的几行代码中实现霍恩逻辑的验证是一个简单的练习。从Vanilla元解释器开始，然后修改它以使用标准的unify_with_occurs_check/2谓词进行所有的统一，并使用完整的搜索过程--迭代深化深度优先搜索是最简单的实现方法。

请参阅@mat的页面Prolog中的几个元解释器，以获得一些灵感。

Answer 2

更多的指示：

• 数据录具有声明性语义，但作为“没有函数符号的Prolog”，它不是Prolog。参见由Ceri，Gottlob和Tanca，1989的精彩的介绍“您一直想知道的关于Datalog (而且从来不敢问)”。可通过CiteSeerX获得
• Prolog的实现使用制表而不是深度优先搜索添加的声明性(以及我理解的其他好特性)，比如XSB。