open-source - GNU Prolog 的重言式检查器

Question

关闭。这个问题不满足Stack Overflow guidelines .它目前不接受答案。












想改善这个问题吗？更新问题，使其成为 on-topic对于堆栈溢出。

6年前关闭。




Improve this question




我要找 开源 用 GNU Prolog 编写的重言式检查器的实现(SWI-Prolog 的实现也是可以接受的，但 GNU Prolog 是首选)。

我想使用以下查询来提供程序输入:

A and (B or C) iff (A or B) and (A or C).

或者

3^2 * (X + 2) == (9 * X) + 18.

当然，符号可以不同，像这样:

(3 power 2) mul (X plus 2) equals (9 mul X) plus 18.

我期望的结果是 bool 答案，例如“是/否”、“等于/不同”、“证明找到/未能找到证明”或类似的。

我在 ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/ 上找到了 GNU-Prolog 的重言式检查器，但没有附上许可证，也不知道如何申请 Gnu Prolog Arithmetic constraints和 Arithmetic功能，以便仅使用算术扩展逻辑模型。

还有其他类似的求解器吗？

一些如何使用算术能力来扩展模型的例子。

谢谢，格雷格。

附注根据算术，我正在寻找部分支持 - 我只想处理一些基本情况，我可以使用简单的启发式方法手动编码(也欢迎 gnu-prolog 整数函数示例)，如果提出的解决方案将正确处理经典逻辑并开放 -源代码将很好扩展:)。

P.P.S 正如@larsmans 所指出的，根据 Gödel's incompleteness theorems没有办法证明“所有”公式。这就是为什么我正在寻找可以证明的东西，可以从给定的公理和规则集证明什么，因为我正在寻找 Gnu Prolog 程序，我正在寻找此类公理和规则集的示例 ;)。当然检查器可能会失败-我希望它可以在“某些”情况下工作:)。 - 另一方面，有 Gödel's completeness theorem ;)

Answer 1

如果您想要 Prolog 中的可扩展定理证明器，请查看精益定理证明器系列，其中 leanCOP是主要代表；它在 555 字节的 Prolog 中处理经典的一阶逻辑。

1.0 版是以下程序:

prove(M,I) :- append(Q,[C|R],M), \+member(-_,C),
 append(Q,R,S), prove([!],[[-!|C]|S],[],I).
prove([],_,_,_).
prove([L|C],M,P,I) :- (-N=L; -L=N) -> (member(N,P);
 append(Q,[D|R],M), copy_term(D,E), append(A,[N|B],E),
 append(A,B,F), (D==E -> append(R,Q,S); length(P,K), K<I,
 append(R,[D|Q],S)), prove(F,S,[L|P],I)), prove(C,M,P,I).

LeanCOP 网站有更多可读版本，具有更多功能。您必须自己实现平等和算术。