问题标签 [minikanren]

这是一个矛盾：

因为不可能同时存在trueaq false。

这不应该也是矛盾的吗？

我不知道那是什么:-意思。但由于地图键是唯一的，我想不可能有一个地图:k必须true和false. 如何确保第二个目标不匹配？

另一个例子

我将其解释为：

• x是与:kas类似的地图false。
• q是true。
• q是的:k值x

我到底想做什么？

我正在尝试用来featurec创建目标，例如：

然后我想说：

想象一下，我的厨房里有许多不同菜肴的食谱和一个装有各种食材的储藏室。我想构建一个模型core.logic，使我能够回答以下问题：对于给定的一组成分（即现在我储藏室中的那些），我可以制作哪些食谱？

食谱有些灵活，我需要能够对此进行建模。稍后我想为它们添加数量，但为了开始，让我们暂时忽略它。

我可以看到如何为储藏室建模：

食谱有一个名称和一个成分列表，可以是可选的或以各种方式组合。有n 个食谱。例如，食谱可能（非正式地）如下所示：

我正在努力解决如何用core.logic. （注意，上面的文字只是说明性的，并不是机器可读的。）

我想查询看起来像这样：

这将返回以下结果（给定上面的储藏室定义）：

我的问题是：如何对这些食谱进行建模，以便我可以对食谱和储藏室编写查询，以列出给定储藏室当前内容的可能食谱的名称？

当我想阅读逻辑编程时，我总是会偶然发现两种“主要”方法：

• miniKanren是The Reasoned Schemer中引入的一种迷你语言，由于core.logic而在当时很流行。
• Prolog，第一个“大”逻辑编程语言。

我现在感兴趣的是：两者之间的主要技术差异是什么？它们在方法和实现上是否非常相似，或者它们采用完全不同的逻辑编程方法？它们来自数学的哪些分支，理论基础是什么？

理解MicroKanren DSL的核心术语有点困难。第 4 节说：

语言的术语由unify操作员定义。在这里，语言的术语由变量、在 下被视为相同的对象eqv?以及上述内容的对组成。

但他们从不描述“对”的实际含义。对是否应该表示两个子项的相等性，如下所示：

所以像这样的术语：

生成一对(≡ a 7)?

编辑：经过进一步考虑，我认为不是这样。论文中提到“pair”似乎要晚得多，对基本系统进行了扩展和改进，这意味着这些对在基本介绍的术语中没有任何意义。这个对吗？

最近我一直在研究像 Neo4j 这样的图形数据库以及 Prolog 和 miniKanren 中的逻辑编程。从我目前所学的来看，两者都允许指定事实和它们之间的关系，还可以查询结果系统以获取一些选择。所以，实际上我看不出它们之间有多大区别，因为它们都可以用来构建图形和查询它，但是使用不同的语法。但是，它们被呈现为完全不同类型的软件。

除了数据库可能提出更时空有效的存储技术的技术性，以及像迷你看人这样的微小逻辑核心更简单和可嵌入之外，如果它们都只是一个图数据库，那么图数据库和逻辑编程语言之间的实际区别是什么+ 查询 API？

这是我关于 Stack Overflow 的第一个问题。

我是逻辑编程的新手，正在尝试评估它是否可以用来解决我正在处理的一些匹配问题。

问题：

假设我们有一个看起来像这样的集合 A。

然后我们还有一些看起来像这样的其他集合。

我要解决的问题是，

“找到与我们所知的其他集合相比，与集合 A 共享最多成员的集合。”

这种情况下的答案应该是集合 D，因为它与集合 A 共享三个成员。与仅与 A 共享两个和一个成员的其他集合相比。

问题一：

逻辑编程能解决这类问题吗？

问题2：

如果可以，您将如何在例如 Clojure 的 core.logic 中做到这一点？

在推理的方案中，他们命名标准 lisp 函数的末尾带有一个“o”，例如consoand appendo。

我的问题是：为什么“The Reasoned Schemer”会在其函数末尾添加一个“o”？

在练习（或条目？）57 中，我只是不明白逻辑是如何流动的。问题是：给定

其中 '=' 实际上是三连杆统一 (?) 运算符。运行以下：

书中给出了答案：

我原以为答案是：

我的理由是 (teacupo x) 中的“x”应该首先通过其所有解决方案，并统一到其所有解决方案的列表中。但似乎teacupo 一次只放弃了一种解决方案。它让我感到困惑，因为我对 conde 的解释是，使用它给出的规则，你应该遍历 conde 的行，在一行成功后，假装它失败，刷新变量并找到下一行成功。鉴于解决方案的工作方式，该代码中的 conde 似乎回到了成功的行，然后迫使 teacupo conde 失败并放弃下一个可能的值。再一次，我会认为 teacupo 解决方案会放弃列表中的所有 conde 解决方案，然后继续进行外部 conde 调用。

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

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

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

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

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

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

...我该如何避免呢？

返回

我理解这意味着_0地图必须至少包含:a 1键值对和:a 2键值对。这似乎是矛盾的，因为:a不能同时映射到两者1，2除非我们使用 MultiMaps。我不能把它读成:a 1OR :a 2，因为我指定的约束是一个连词。我原以为结果应该是()因为约束是矛盾的；没有任何价值q可以满足这些约束。

我一定是读错了结果。