Prolog后继符号得到的结果不完整并导致无限循环。
我开始学习Prolog，并了解了后继符号。 这就是我了解在Prolog中编写Peano公理的地方。 请参阅PDF第12页：sum(0, M, M). sum(s(N), M, s(K)) :- sum(N,M,K). prod(0,M,0). prod(s(N), M, P) :...
我该如何在Coq中将“+1”（加一）重写为“S”（后继）？
我有一个引理，但证明不完整： Lemma s_is_plus_one : forall n:nat, S n = n + 1. Proof. intros. reflexivity. Qed. 这个证明失败了： Unable to unify "n + 1" with "S n...
在Prolog中将Peano数s(N)转换为整数
我在教程中看到了这个逻辑数字的自然数评估，它让我有些头疼： natural_number(0). natural_number(s(N)) :- natural_number(N). 这个规则大致说明：如果 N 是 0，那么它是自然数；否则我们尝试递归地将 s/1 的内容发送回规则，直到...
Prolog中的s()谓词是什么？
我一直在尝试学习Prolog，但是对于谓词s()的作用完全不了解。我经常看到它被使用，但是因为Prolog相关的资源非常少，我无法找到答案。例如： /* sum(Is,S) is true if S is the sum of the list of integers Is. ...
如何防止Prolog无限制地检查不可能的解决方案？
假设以下程序： nat(0). nat(s(N)) :- nat(N). /* 0+b=b */ plus(0,B,B) :- nat(B). /* (a+1)+b = c iff a+(b+1)=c */ plus(s(A),B,C) :- plus(A,s(B),C). 它非常适用...