我正在开发一个群论证明器。现在，我有兴趣证明如果H和K是子群，那么H与K相交是子群。我的证明基于构造一个关系式(==H(，使得
h(==h(g当且仅当hg^{-1}属于h。证明这是等价关系(自反、对称、传递(等价于证明h是子群。
我已经完成了下面的代码，当我试图证明H相交K是子群时，我失败了。我是Prolog的新手，所以也许我有一些基本的错误。在数学证明中，不需要说等价关系的显式，因此我省略了它
在程序中，我将hg和kg表示为H和K。H与K相交，K为hkg。
inside(X,H) :- equals(H,X,e).
equals(hkg,e,e).
equals(hkg,x,e).
equals(hkg,y,e).
equals(hkg,z,e).
equals(hkg,X,Y) :- equals(hg,X,Y),equals(kg,X,Y).
reflexive(H) :- forall(inside(X,H),equals(H,X,X)).
symmetric(H) :- forall(equals(H,X,Y),equals(H,Y,X)).
transitive(H) :- forall(equals(H,X,Y),equals(H,Y,Z),equals(H,X,Z)).
subgroup(H) :- reflexive(H),symmetric(H),transitive(H).
subgroup(hg).
subgroup(kg).
目前，它未通过自反性测试(第一次测试(。你能告诉我这个节目出了什么问题吗？如果你需要更多的澄清，请随时询问。
Prolog对定理证明并不那么好。它在逻辑程序中调用谓词的方式是基于解析定理证明的(因此仅限于Horn子句(，但这并不意味着该语言允许您对定理证明问题建模；技术特别好。特别是因为Prolog处理目标p(X,Y)，它试图找到使这些目标如逻辑程序所定义的那样为TRUE的元组(x,y)，而不是处理根据某些逻辑(经典、直觉等(的一些推导方法(自然推导、序列演算(重写的句子S，直到获得最终的S'。特别要注意的是，在任何地方都看不到量词，因为没有人编写可能需要它的S。这并不意味着不能在Prolog上构建定理证明器，但有一些方法可以实现。
在这种情况下，对于
reflexive(H) :- forall(inside(X,H),equals(H,X,X)).
你已经有麻烦了，因为Prolog证明reflexive(hg)意味着
实际上去寻找任何X，这样inside(X,hg)
inside(X,hg) :- equals(hg,X,e).
实际上去寻找任何X，这样equals(hg,X,e)
因为我需要确保inside(X,hg)(以及语句∀X:equals(hg，X，e(=>内部(X，hg(将允许我这样做(
在这个逻辑程序中没有。
反射性应该是空洞真实的
?- reflexive(hg).
true.
不错，但没用。