prolog编写群论公理，并实现代数学定理自动证明

有没有人尝试过用 prolog 编写（比如）三条群论公理，并实现代数学定理自动证明。

更多信息见网址discuss.visual-prolog.com/viewtopic.php?t=9340&highlight=

我记得P99: Ninty-nine Prolog Problems有一些题目是试解古典逻辑问题，包括写个逻辑式的真值表等等。基本稍微把 and, or, not, imply, equal 这些运算单元定义清楚就够了。

不过，在2006年知识系统期刊 (名称没记清楚，貌似Journal of Expert Systems) 冬季号，有位学者 James D. Jones 整理电脑程式的逻辑系统，提到 Prolog 属於 Monotonic Logic System ，有 closed world assumption 的特性。

文章名称见以下超连结，
http://onlinelibrary.wiley.com/doi/10.1111/j.1468-0394.2006.00415.x/abstract

我忘了古典逻辑是否也都是 closed world assumption ，不过既然 Prolog 是演绎式的逻辑环境，要用来操作古典逻辑时，应该没有多少障碍。

---

後补充：发帖之後才发觉是问群论 (Group Theory) 。 Prolog 可能是个好基础，貌似也可使用函数式编程的 Haskell 。

先是题外话，请问你是你说的更多信息网址的发帖人lambda吗？

就lambda他的问题来讲，想要表达任何一个元素对根本元素拥有反元素，以参考了这个教程 ( http://dogschool.tripod.com/groups.html ) 为基础，我的办法是先把教程的基本资料翻译为 Prolog 程序。

群论的公理规则说：

1. 基础：一个群存在一个根本元素，并且对一项操作构成一个群。在此称此操作为 op 。
   
2. 小圈圈：假如 A 和 B 在这个群中，则 A op B 也属於这个群。
   
3. 黏合：前提说 A, B, C 都在群中，假如有个式子为 (A op B) op C ，则也会有个式子为 A op (B op C ) ，相对来讲，假如有个式子为 A op (B op C ) ，则也会有个式子为 (A op B) op C 。
   
4. 一致性：再说前提有根本元素称为 e ，假如有个式子为 A op e ，则也会存在有 A 跟那个式子一致，或者假如有个式子为 e op A 也是跟 A 一致。要反过来表达 A -> A op e 及 A -> e op A 也可以，但写成 Prolog 时，如果要同时描述前者、後者，要小心避免无限递归。
   
5. 反元素：这也是说前提是都把 A 的反元素称为 A^(-1) ，则假如 A op A^(-1) 存在，则此式可以代换为 e 。
   

这些规则要转写成 Prolog 程序，可以有很多种写法，你可以把 op 定义成原子，或者把式子写在列表中。不过基本一定从这种练习开始，先就 Prolog 的运行方式，把理论的定义翻抄一次，像我这样：

代码:

element(one).
times(one, N, one*N).
times(N, one, N*one).
% Closure
times(A*B, N, (A*B)*N) :- times(A, B, A*B).
times(N, A*B, N*(A*B)) :- times(A, B, A*B).
% Associativity
times(A*B, C, A*(B*C)) :- times(A*B, C, (A*B)*C).
times(A, B*C, (A*B)*C) :- times(A, B*C, A*(B*C)).
% Identity
times(A, E, A) :- element(E).
times(E, A, A) :- element(E).
% Inverses
times(A, 1/A, E) :- element(E).
times(1/A, A, E) :- element(E).


虽然距离你所说，「自动证明」，差了一大段路，但是对於lambda所提的那个问题 "how to express the fact that any element in group has a inverse" 可能下面几行都可以是一些解答：

代码:


?- times(A, 1/A, X). %持续演绎，符合各种情况
A = one,
X = one* (1/one) ;
A = one*_G3468,
X = one*_G3468* (1/ (one*_G3468)) ;
A = _G3467*one,
X = _G3467*one* (1/ (_G3467*one)) ;
A = one*_G3480*_G3468,
X = one*_G3480*_G3468* (1/ (one*_G3480*_G3468)) ;
A = _G3479*one*_G3468,
X = _G3479*one*_G3468* (1/ (_G3479*one*_G3468)) ;
A = one*_G3486*_G3480*_G3468,
X = one*_G3486*_G3480*_G3468* (1/ (one*_G3486*_G3480*_G3468)) ;
...
?- times(A, B, one). %查询结果的最後二句是由反元素规则引出
A = B, B = one ;
A = B, B = one ;
B = 1/A ;
A = 1/B.


在表达结合律的时候是否可以再简练一点，直接
times(A*B, C, A*(B*C)). 或者A*(B*C) is (A*B)*C.

还有为什么不直接times(a,1/a,one). 如果要防止循环可以cut

function 写道:在表达结合律的时候是否可以再简练一点，直接
times(A*B, C, A*(B*C)). 或者A*(B*C) is (A*B)*C.

还有为什么不直接times(a,1/a,one). 如果要防止循环可以cut

这看你要证明的目标是什麽。因我没有所证明的目标，只求简单表达各律。不同的程序各有精简的方面，不需特别求共同的绝对精简。我建议你先明确定义你要证明的目标和前提，才讨论程序应怎麽写。

至於A*(B*C) is (A*B)*C，应不是成立的句子。

代码:

?- A=1, B=2, C=3, A*(B*C) is (A*B)*C.
false

function 写道:在表达结合律的时候是否可以再简练一点，直接
times(A*B, C, A*(B*C)). 或者A*(B*C) is (A*B)*C.

如果写成

代码:

times(A*B, C, A*(B*C)).

会让人误认为是你定义的乘法比较特别。

应该写成如此即可：

代码:

% Associativity
% For all a, b and c in G, (a • b) • c = a • (b • c).
imply(times(times(A,B),C), times(A,times(B,C))).
imply(times(A,times(B,C)), times(times(A,B),C)).