我开始学习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) :...

到目前为止，我一直认为Prolog程序中的坚定性意味着： 如果对于一个查询Q，存在一个子项S，使得存在一个术语T使得?- S=T, Q.成功，尽管?- Q, S=T.失败，那么由Q调用的谓词之一是不坚定的。 直观地说，我认为坚定性意味着我们不能使用实例化来“欺骗”谓词以提供否则不仅从未...

CPDT的第三章简要讨论了为什么Coq中禁止负归纳类型。如果我们有 Inductive term : Set := | App : term -> term -> term | Abs : (term -> term) -> term. 那么我们可以轻松地定义一个...