问题标签 [successor-arithmetics]

我有以下引理，但证明不完整：

这个证明失败了

这似乎eq_S是证明这一点的方法，但我不能应用它（它不能识别n + 1为S n: Error: Unable to find an instance for the variable y.）。我也试过ring了，但找不到关系。当我使用rewrite时，它只是减少到相同的最终目标。

我怎样才能完成这个证明？

我有以下知识库，应该添加两个参数并给出结果：

现在这是我的查询：

0 不与第一个参数统一，因此它转到第二个 add/3 子句。现在这是我无法弄清楚的事情。这本书（LPN）告诉我，最外层的成功因素被排除在第一个参数之外，但我不知道为什么？在我看来，它增加了一个 succ 仿函数。有人可以解释一下为什么要剥离它吗？

提前致谢！

卢克

我正在玩 DCG，我有这个代码。这将显示s 的x数量和s 的数量。0xA

我的问题是如何通过函子使As 的数量成为 s 的数量的两倍0。这是我尝试过的，但它不起作用。

如果我只想添加一个，这就是它所做的并且工作正常。

我无法理解此示例中发生的情况
立即学习 Prolog -第 3 章- 示例 3：继任者

当询问 numeric(X) 时，它会首先为 X 给出 0，然后继续 succ(0)，以这种方式将 succ(0) 部分递增 1，直到它用完空间：

我很难理解为什么它会增加 succ(0)？

我知道序言会首先找到一个事实并匹配它，因此是第一个 0。然后它会回溯以查看是否有任何其他解决方案，它会“看到”规则。在规则中，它将使用实例化的 X 为 0。我失败的地方是看看为什么它会不断增加 succ(0)。X 是否变为 succ(0)，而不仅仅是 0？

我为愚蠢的大脑道歉。

我正在学习 Prolog。我正在试验一个elemindex谓词，形式elemindex(element, index, list)为 ，例如，elemindex(1,0,[1,2,3,1]).或elemindex(3,0,[1,2,3,1]).。

由于实例化限制，我最终得到了这个：

但是，如果我查询?- elemindex(1,N,[1,2,3,1]).，如我的示例所示，Prolog 会响应：

这当然有效，但我想s(s(s(0)))至少显示为3. 此外，我无法执行类似的查询?- elemindex(E, 3, [1,2,3,4]).，但是更改要使用的代码N is M+1会使我失去评估第一种查询的能力。

所以，我的问题有两个：

1. 我怎样才能在我的结果s(s(s(0)))中显示3？
2. 我怎样才能实现elemindex这样我可以查询元素和索引？

这就是我使用谓词加号和大于号的原因。但是，我想使用谓词、时间和加号来实现这一点。

PS：

知识库

询问

痕迹

我的问题

• 我看到第 2 条中的递归调用如何在每次调用参数 1 时剥离最外层的 succ()。
• 我看到它如何在每次调用时将外部 succ() 添加到参数 3。
• 我看到作为这些递归调用的结果的第一个参数何时达到 0。此时，我看到第一个子句如何将第二个参数复制到第三个参数。

这就是我感到困惑的地方。

1. 执行第一个子句后，第二个子句是否也会自动执行，然后将 succ() 添加到第一个参数？

2. 另外，程序是如何终止的，为什么它不只是无限地向第一个和第三个参数添加 succ() 呢？

LearnPrologNow.com 的解释（我不明白）

让我们逐步了解 Prolog 处理此查询的方式。查询的跟踪和搜索树如下所示。

第一个参数不是 0 ，这意味着只能使用 add/3 的第二个子句。这导致 add/3 的递归调用。最外层的 succ 函子被剥离了原始查询的第一个参数，结果成为递归查询的第一个参数。第二个参数不变地传递给递归查询，递归查询的第三个参数是一个变量，即下面给出的跟踪中的内部变量 _G648。请注意，_G648 尚未实例化。然而，它与 R（我们在原始查询中用作第三个参数的变量）共享值，因为当查询与第二个子句的头部统一时，R 被实例化为 succ(_G648)。但这意味着 R 不再是一个完全未实例化的变量。现在是一个复杂的术语，

接下来的两个步骤基本相同。每一步，第一个参数都会变小一层 succ；下面给出的跟踪和搜索树都很好地说明了这一点。同时，每一步都将一个 succ 函子添加到 R 中，但始终不实例化最里面的变量。在第一次递归调用后 R 是 succ(_G648) 。在第二次递归调用后，_G648 被 succ(_G650) 实例化，因此 R 为 succ(succ(_G650) 。在第三次递归调用后，_G650 被 succ(_G652) 实例化，因此 R 变为 succ(succ(succ( _G652))) . 搜索树显示了这个一步一步的实例化。

在这个阶段，所有的 succ 函子都被剥离了第一个参数，我们可以应用 base 子句。第三个参数等于第二个参数，所以复数 R 中的“洞”（未实例化的变量）最终被填满，我们通过了。

我不明白为什么这个乘法的递归定义是有效的。
我得到了添加部分，但在这种情况下“A”的值如何。代码如下：

我想在 Prolog 中从自然数创建后继数。

输出应该是这样的：

实际上它是一个不定式循环。我不知道如何结束循环而不只是得到真实的结果。

首先，我对 prolog 完全陌生，我正在尝试编写一个谓词长度（M，X，N），如果 M 与 N 的差异大于 X，则该谓词长度（M，X，N）是正确的。

我编写了以下测试用例，如果 M(=dec.5) 和 N(=dec.2) 的差异大于 X(=dec.2)，则该测试用例为真。在这种情况下是正确的，因为 5 和 2 相差 3 大于 2：

我知道 prolog 是递归工作的，所以我想知道我是否可以像 C 语言那样用条件（例如 <，>）构造这样的谓词，或者在 prolog 中是否有另一种方法可以做到这一点。很抱歉这个简单的问题，但我刚从序言开始。