An equilateral triangle has six symmetries: three rotations (including doing nothing) and three reflections. Together they form the group D3. EyeProlog generates every subset of the six, keeps the ones closed under composition and inverse, and finds exactly six subgroups.
Run it in the playground · Source
A subgroup is a subset that is a group in its own right. It contains the identity, it is closed under composition (combining two members gives a member), and it contains the inverse of each member.
D3 has 2⁶ = 64 subsets. Which of them pass all three tests?
symmetry(identity).
symmetry(rotation_120).
symmetry(reflection_a).
compose_op(rotation_120, rotation_120, rotation_240).
compose_op(rotation_120, rotation_240, identity).
compose_op(reflection_a, reflection_b, rotation_240).
inverse(rotation_120, rotation_240).
inverse(reflection_a, reflection_a).
compose_op/3 is the Cayley table: all 36 products of two symmetries, written
out as facts. inverse/2 pairs each symmetry with the one that undoes it. (A
few rows of each are shown.)
closed_under_composition(Group) :-
\+ (member(X, Group), member(Y, Group), compose_op(X, Y, Z), \+ member(Z, Group)).
valid_group(Group) :-
all_symmetries(All),
subsequence(All, Group),
member(identity, Group),
closed_under_composition(Group),
closed_under_inverse(Group).
all_subgroups(Groups) :-
findall(G, valid_group(G), Raw),
sort(Raw, Groups).
“Closed” is written as the absence of a counterexample: there is no pair in
the group whose product falls outside it. subsequence/2 generates the 64
candidates, the tests filter them, and findall/3 with sort/2 collects the
survivors in a canonical order.
eyeprolog examples/d3-group.pl
subgroups(d3_group, [[identity], [identity, reflection_a], [identity, reflection_a, reflection_b, reflection_c, rotation_120, rotation_240], [identity, reflection_b], [identity, reflection_c], [identity, rotation_120, rotation_240]]).
subgroupCount(d3_group, 6).
The six subgroups are the trivial group, the whole of D3, the rotations, and three two-element groups, each made of the identity and one reflection. The sizes (1, 2, 3, 6) all divide 6, as Lagrange’s theorem says they must.
step(findall(G, valid_group(G), [[identity, reflection_a, reflection_b, reflection_c, rotation_120, rotation_240], [identity, reflection_a], [identity, reflection_b], [identity, reflection_c], [identity, rotation_120, rotation_240], [identity]]),
collected,
[],
[]).
The count rests on one collection: findall/3 gathered every valid_group/1
answer. The proof records that collection as a completed search (collected)
rather than repeating all 64 candidate checks.
condition('C1', resolution, ok, 3).
condition('C5', re_decision, ok, 2).
obligation(collected, theory_scoped, findall(A, valid_group(A), [[identity, reflection_a, reflection_b, reflection_c, rotation_120, rotation_240], [identity, reflection_a], [identity, reflection_b], [identity, reflection_c], [identity, rotation_120, rotation_240], [identity]])).
steps(6).
trusted(1).
verdict(checked_with_obligations).
The checker verifies the three rule steps and recomputes sort/2 and
length/2. The findall/3 result stays an obligation: claiming that these
are all the subgroups needs the whole search, which the checker does not
redo. The verdict is honest about that: the proof holds, provided the
collection is complete.
closed_under_inverse(Group) test. The count stays at 6. Why does
closure under composition already force inverses in a finite group?member(identity, Group) instead. The count becomes 7. Which extra
“subgroup” slips through?Learn more in The Art of EyeProlog, Chapter 28 (algebra, symmetry, and representation).