prolog - 如何实现完全声明式的 Horn 逻辑？

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

6年前关闭。




Improve this question




我想正式化一些知识并在可能称为完全声明性的内容中执行查询 Horn logic (或者，完全声明性的 Prolog)。谁能提供一些关于如何实现它的指导方针？我简要回顾一下上面链接中的精美描述:

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

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

展会 搜索匹配规则(例如，Prolog 的深度优先搜索是 而不是 公平)；

与“ 发生-检查”的统一(检查变量没有出现在与其统一的术语中)。

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

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

Answer 1

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

见@mat 的页面 A Couple of Meta-interpreters in Prolog一些灵感。