问题标签 [unification]

我正在研究一个高阶定理证明器，其中统一似乎是最困难的子问题。

如果 Huet 的算法仍然被认为是最先进的，那么有没有人有任何链接到它的解释，这些解释是为了让程序员而不是数学家理解的？

或者甚至是它在哪里工作而通常的一阶算法不工作的任何例子？

我正在编写一个谓词来查找 A* 迭代的所有可能的后继状态，并将它们放在像 [(cost, state), ...] 这样的列表中，目前该列表如下：

Add 将某些内容添加到列表的末尾， memb 获取列表的第（索引）个元素。我知道它们有效，当我查看底部谓词中的 L2 时，我会得到这样的结果

这非常令人沮丧，因为 [(1500, 3), (3670, 4)] 列表是我在调用它之后希望 X 成为的列表​​，所以它看起来正在做我想做的事情，而不是......我想要的地方。

请问，我该如何解决这个问题？

为什么在 C# 中不允许这样做？ 替代文字 http://img706.imageshack.us/img706/7360/restriction.png

其实我希望能够写作

这里实际上需要统一；如果 A = B 则只应定义一种方法。

我知道这只是编程问题的一部分，但目前，我正在做一些逻辑编程。我仍然无法正确理解的一件事是一阶逻辑中的统一。

我阅读了维基百科的文章，或多或少地清楚目的是搜索一个统一两个句子的术语......本文中也有示例，但我只是不明白为什么这应该有用。任何人都可以用现实世界的对象而不是 A、B、C 等举个例子吗？我希望这能帮助我理解。谢谢

在 prolog 中，我们可以执行以下操作：

也就是说，当 的第一个参数myFunction与第二个参数中的列表的第一项相同时，此函数的计算结果为...。

我现在的问题是......如何在 Haskell 中完成类似的事情？我认为 Prolog 的模式匹配比 Haskell 的更具表现力。我一直在尝试在 Haskell 中编写代码，但遇到了麻烦——要么我使用了无效的语法，要么上述技巧根本行不通。

假设我有以下规则：

然后我按如下方式运行它：

为什么 SWI-Prolog 统一test和'test'到unify('test', 'this is a test').？我在回答关于 SO 的 Prolog 问题时遇到了这个问题。虽然我能够回答这个人的问题，但我无法解释这种特殊行为，我想知道其他人是否可以。

我正在开发（在 Java 中），为了好玩，一个使用统一算法的应用程序。

我选择我的统一算法返回所有可能的统一。例如，如果我尝试解决

添加（X，Y）=成功（成功（0））

它返回

{X = succ(succ(0)), Y = 0}, {X = succ(0), Y = succ(0)}, {X = 0, Y = succ(succ(0))}

然而，在某些情况下，可能存在无限多的统一（例如 X > Y = true）。

有人知道算法允许确定是否可能遇到无限数量的统一吗？

提前致谢

从我班的旧决赛中：

这是一些序言代码：

问题一：P中的什么值统一

问题2：如果Prolog产生并回答神秘问题后按下分号，解释器最终会报告“ERROR：Out of local stack”。为什么会发生这种情况，您如何修改谜题以避免错误？

问题1：我明白了

问题 2：如果我按分号来获取所有答案，我会得到一个 out of local stack 错误。我不确定这段代码试图完成什么或如何修复它，所以我不会离开本地堆栈。有任何想法吗？

我以为我了解在 Scala 和 Haskell 中发现的模式匹配与在 Prolog 中发现的统一性有何不同，但我对 Prolog 的误解很大。有哪些简单的问题可以由一个人解决而另一个人无法解决？谢谢

好吧，我知道这听起来可能有点奇怪，但是我的问题是：“什么是统一算法”。好吧，我正在尝试在 F# 中开发一个应用程序来像 Prolog 一样工作。在进行查询时，它应该采用一系列事实并对其进行处理。

有人建议我开始实施一个好的统一算法，但对此一无所知。

如果您想更深入地了解我想做的事情，请参考这个问题。

非常感谢你，圣诞快乐。