如何实现完全声明性的 Horn 逻辑？ [关闭]答案

【问题标题】：How to implement fully-declarative Horn logic? [closed]如何实现完全声明性的 Horn 逻辑？ [关闭]
【发布时间】：2015-10-18 22:07:26
【问题描述】：

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

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

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

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

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

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

【问题讨论】：

要求我们推荐或查找书籍、工具、软件库、教程或其他非现场资源的问题对于 Stack Overflow 来说是题外话，因为它们往往会吸引固执己见的答案和垃圾邮件。
我不是在寻找意见。我正在寻求帮助以找到我无法找到的东西，或者一些关于如何自己做的指南（例如，miniKanren）。
@amka00 - 这是我评论的“寻找”部分。
公平搜索规则并不是那么有趣，毕竟它们保证在存在的情况下找到答案/解决方案，但如果没有答案，它们通常不会终止。

标签： prolog theorem-proving logic-programming formal-verification minikanren

【解决方案1】：

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

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

【讨论】：

【解决方案2】：

更多指点：

Datalog 具有声明性语义，但作为“没有函数符号的 Prolog”，它不是 Prolog。请参阅 Ceri、Gottlob 和 Tanca 于 1989 年撰写的精彩介绍“您一直想知道的关于 Datalog 的内容（而且从来不敢问）”。可通过 CiteSeerX
Prolog 的实现使用 tabling 而不是深度优先搜索来增加声明性（加上我理解的其他不错的功能），例如 XSB。

【讨论】：