问题标签 [unification]

我有以下条款：

我的问题是关于统一的。例如：“3”是否会与“p(X)”统一[一些 p，atm 无关紧要]

现在，我的直觉是这样的：第一学期将统一（X = 3）第二学期将统一（X = 3）第三学期我不确定，我认为它也会......（As _ = 3）

任何人都可以为我阐明这一点吗？谢谢

我正在尝试创建自己的 WAM 实现，但我被困在练习 2.4

我无法理解如何执行unify_value X4图 2.4 中的指令。

据我了解，该指令应将程序中的 Y 与查询中的 f(W) 统一起来。

unify_value X4调用unify (X4,S)其中 S=2（参见图 2.1）并且相应的堆单元是“REF 2”，而 X4 是“STR 5”。

Unify（图2.7）应该bind是那些值，但是我不明白怎么deref注册。

“REF 2”在堆中，“STR 5”在寄存器中。你怎么bind注册？

我试图在 SMT-LIB 中执行此操作，z3 -smt2 script.smt2在包含这些表达式的脚本上运行：

我想统一这些变量。例如，我希望能够通过分配x=f,a=d和来统一变量b=e。

z3甚至有可能在or中做到这一点SMT-LIB？

或者我应该使用其他语言来做到这一点（也许给出建议是你的想法？）

我是遵循“LearnPrologNow！”的 Prolog 初学者。一套教程。我正在尽我所能掌握概念和词汇。当遇到这个问题时，我已经能够理解所有内容，直到第 3 章递归定义：

给定查询

现在，我了解到该程序的想法是 Prolog 将开始在该系统中按以下顺序计数数字

但我不明白是什么导致它每次“缩减”并上升。我理解统一的原则是程序试图统一X的查询，但是它应该只遵循递归规则一次，然后返回零吗？是什么允许它在查询周围添加一个 succ() ？那不是在相反的方向遍历递归规则吗？

谁能帮我证明：

公式 F 的一个实例的全封闭是 F 的全封闭的逻辑结果。

谢谢。

我正在研究“猴子和香蕉”问题，但用的是 2 盒而不是 1 盒。我尝试将代码从 1 个盒子调整为 2 个盒子，但我遇到了这个问题。

我需要保留一个“访问过的状态”列表，因为树变得太大并且我的程序崩溃了。在这个列表中是从开始到实际状态的所有已访问状态，因此如果我要进入已访问状态，则该子句将失败并发生回溯。

问题是有时会发生这种情况：

在尝试查找所有可能的状态时，我需要检查所有可能的位置（例如：门（puerta）、窗口（ventana）和中间（centro）），但由于变量没有实例化，显然它们统一和成员（状态， List) 返回 true，因此程序回溯，我从不检查所有可能的状态。

我尝试使用 \== 检查成员资格，但发生了其他问题：由于状态（带有未实例化的变量）总是不同的（状态（_G1234）与状态（_2345）不同）我进入一个无限循环并且永远不会结束，因为它正在检查许多具有未实例化（但不同）变量的状态。

我怎么能解决这个问题？还是我应该尝试另一个近似值？我考虑过定义“位置”的预设，但我不确定在执行规则时如何检查所有不同的位置。

规则是这样的：

其中 estado(P, p0, P1, P2, A, E) 表示：

1. 猴子的位置（X 轴）。
2. 猴子的位置（Y 轴）。
3. 第一个盒子的位置。
4. 第二个盒子的位置。
5. 盒子是否堆叠。
6. 猴子有没有香蕉。

我应该尝试检查所有可能的 PD（猴子的命运位置），但我不知道该怎么做。

提前致谢。

我正在尝试进一步了解 Prolog，以及它如何处理列表统一。所以我坚持这个例子，我在执行代码时知道答案，但我不明白它是如何工作的。

答案是：

我知道头部与另一个头部统一，所以如果我进行一些更改，如下所示：

统一应该这样：

所以 Y 必须等于 L，而不是 _，对吧？有人可以更好地解释我并纠正我的错误吗？

在 Prolog 中，我输入了以下查询以检查它们是否匹配：

Prolog 对此作出回应：

但在书中写道，Prolog 应该这样回应：

为什么会这样？

我正在尝试将变量 X 与 '*' （包括引号，总共 3 个符号字符串）统一我正在做的是一个简单的X='*'.，但这导致 X 具有 value *。如果我去X=''*''.，结果是X=''*''。我很困惑，我该如何实现'*'？