Proving H intersects K is a subgroup in Prolog (H and K are subgroups)

Question

I am developing a group theory prover. Right now, I am interested in proving if H and K, are subgroups, then H intersects K is a subgroup. I base my proof in constructing an relation (==H) such that

h (==H) g if and only if hg^{-1} belongs to H. Proving this is an equivalence relation (reflexive, symmetric, transitive) is equivalent to proving that H is a subgroup.

I have done this following code and when I try to prove H intersect K is a subgroup, I get failure. I am new in Prolog so maybe I get something basic wrong. In the mathematical proof it is not required to say the explicit form of the equivalence relation, hence I have omitted it.

In the program I denote hg and kg as H and K. H intersect K is 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).

For now, it fails the reflexivity test (first test). Could you please show me what is wrong with this program? If you need more clarifications, feel free to ask.

Answer 1

Prolog is not all that good for theorem proving. The way it calls the predicates in the logic program is based on resolution theorem proving (and thus restricted to Horn clauses), but that doesn't mean that the language allows you to model theorem proving problems & techniques particularly well. In particular because Prolog works on goals p(X,Y) for which it tries to find tuples (x,y) that make these goals TRUE as defined by the logic program, rather than work on sentences S that are rewritten according to some deduction approach (Natural Deduction, Sequent Calculus) for some Logic (Classical, Intuitionistic etc.) until the final S' obtains. Note in particular how there are not quantifiers anywhere in sight, because no-one writes the S that may need it. This doesn't mean one cannot build a theorem prover on Prolog, but there is some way to go for that.

In this case for

reflexive(H) :- forall(inside(X,H),equals(H,X,X)).

you are already in trouble, because Prolog-proving reflexive(hg) means

Actually go and find any X such that inside(X,hg)

inside(X,hg) :- equals(hg,X,e).

Actually go and find any X such that equals(hg,X,e)

because I need to make sure inside(X,hg) (and the statement ∀X: equals(hg,X,e) => inside(X,hg) will allow me to do that)

... and there are none in this logic program.

Reflexivity should be vacuously true

?- reflexive(hg).
true.

Nice, but useless.