2

我正在寻找用 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.

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

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

  • 还有其他类似的求解器吗？
  • 一些示例如何使用算术能力来扩展模型。

谢谢，格雷格。

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

PPS 正如@larsmans 所指出的，根据哥德尔的不完备性定理，没有办法证明“所有”公式。这就是为什么我正在寻找可以证明的东西，可以从给定的公理和规则集证明什么，因为我正在寻找 Gnu Prolog 程序，我正在寻找此类公理和规则集的示例；）。当然检查器可能会失败 - 我期待它会在“某些”情况下工作:)。- 另一方面，有哥德尔的完备性定理；）。

4

3 回答 3

3

如果你想要 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).

leaCOP 网站有更易读的版本，具有更多的功能。您必须自己实现相等和算术。

于 2011-08-15T14:42:06.263 回答
1

您可以使用约束逻辑编程来解决您的问题。Equality 直接给你一个结果（例如 GNU Prolog）：

?- X*X #= 4.
X = 2

对于不等式，您通常需要在设置约束后要求系统生成实例。这通常通过标签指令（例如 GNU Prolog）来完成：

?- 27 * (X + 2) #\= (9 * X) + 18.
X = _#22(0..14913080)
?- 27 * (X + 2) #\= (9 * X) + 18, fd_labeling(X).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
Etc..

可以在此处找到显示哪些 prologs 确实具有哪种 CLP 的列表。只需检查 CLP 多列。

Prolog 系统概述，Ulrich Neumerkel

再见

于 2011-08-31T08:54:33.287 回答
0

我在Ben-Ari, Mordechai 的计算机科学数学逻辑中找到了一些重言式检查器，不幸的是它们涵盖了布尔逻辑。有什么优势，他的实现在 Prolog 中，并提供了与自动证明相关的各种方法，或解决此类方程（或自动验证证明）。

于 2011-08-29T22:24:26.917 回答