5

我想形式化一些知识并在可能被称为完全声明性的Horn 逻辑（或完全声明性的 Prolog）中执行查询。谁能提供一些有关如何实施它的指导方针？我简要回顾了上面链接中的详细描述：

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

然而，与 Prolog 相比，我正在寻找一种相对于逻辑程序的标准声明语义而言是健全和完整的实现——最小的 Herbrand 模型（即，归纳定义的一组基本术语）。在逻辑编程的理论工作中，这通常是研究的对象，众所周知，可以（在“递归可枚举”意义上）获得对查询的健全和完整的答案，例如，使用 SLD 解析受以下条件：

  • 匹配规则的公平搜索（例如，Prolog 的深度优先搜索不公平）；
  • 与“发生检查”的统一（检查变量没有出现在与之统一的术语中）。

我正在寻找一种基于现有功能的简洁实现，而不是发明轮子。我看到的两个更有希望的方向是将其实现为 Prolog 的元解释器，或者作为某些定理证明器的一部分。任何具有这些领域实践知识的人都可以就如何实施它提供一些指导吗？能否在miniKanren中轻松实现？

我的意图是以完全声明的方式形式化一些知识。这种形式化的关键特征是它精确地对应于（单调）归纳的数学概念，因此可以很容易地用归纳论证来推理知识及其属性。

4

2 回答 2

7

用几行 Prolog 实现 Horn 逻辑的证明器是一个简单的练习。从 Vanilla Meta-interpreter 开始，然后修改它以使用标准unify_with_occurs_check/2谓词进行所有统一，并使用完整的搜索过程 - 迭代加深深度优先搜索是最简单的实现。

请参阅@mat 的页面A Couple of Meta-interpreters in Prolog以获得一些灵感。

于 2015-07-28T11:34:26.443 回答
2

更多指针：

  • Datalog具有声明性语义，但作为“没有功能符号的 Prolog”，它不是 Prolog。请参阅 Ceri、Gottlob 和 Tanca 于 1989 年撰写的精彩介绍“您一直想知道的关于 Datalog 的内容（而且从来不敢问）”。可通过CiteSeerX 获得

  • Prolog 的实现使用表格而不是深度优先搜索来增加声明性（加上我理解的其他不错的功能），例如XSB。

于 2015-07-31T03:49:05.710 回答