0

我正在开发一个群论证明器。现在，我有兴趣证明如果 H 和 K 是子群，那么 H 与 K 相交是子群。我的证明基于构建一个关系（==H），使得

h (==H) g 当且仅当 hg^{-1} 属于 H。证明这是一个等价关系（自反、对称、传递）等价于证明 H 是一个子群。

我已经完成了以下代码，当我尝试证明 H intersect K 是一个子组时，我失败了。我是 Prolog 的新手，所以也许我遇到了一些基本错误。在数学证明中不需要说等价关系的显式形式，因此我省略了它。

在程序中，我将 hg 和 kg 表示为 H 和 K。H 相交 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).

目前，它没有通过反身性测试（第一次测试）。你能告诉我这个程序有什么问题吗？如果您需要更多说明，请随时询问。

4

1 回答 1

1

Prolog 对于定理证明并不是那么好。它在逻辑程序中调用谓词的方式基于解析定理证明（因此仅限于 Horn 子句），但这并不意味着该语言允许您特别好地建模定理证明问题和技术。特别是因为 Prolog 在目标上p(X,Y)工作，它试图找到(x,y)使这些目标为逻辑程序定义的 TRUE 的元组，而不是在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) => inside(X,hg)将允许我这样做）

...这个逻辑程序中没有。

反身性应该是空虚的

?- reflexive(hg).
true.

很好，但没用。

于 2020-04-06T11:42:58.740 回答