Question: Meaning of SymmetryGroup in the Logic package

I am trying to understand the SymmetryGroup returned in the Logic Package. The help page says "The group is a permutation group; its elements are those permutations which preserve the Boolean structure of expr." [my bold], but later the definition is given as "A symmetry of a Boolean expression expr is a mapping f of each variable to some other variable or negated variable, such that the image of expr after applying f to each of its variables is a Boolean formula which is equivalent to expr." Is logically equivalent meant here, or something else? The help page examples don't answer this question.

The following example shows that a group permutation does not lead to a logically equivalent statement as I was expecting - is this a bug, or am I expecting too much here?



q := `&and`(`&or`(x[1], x[2]), x[3])

Logic:-`&and`(Logic:-`&or`(x[1], x[2]), x[3])

G, L := SymmetryGroup(q, output = [group, expressions]); g1, g2 := Generators(G)[]

_m1897409254784, [x[1], x[2], x[3], Logic:-`&not`(x[1]), Logic:-`&not`(x[2]), Logic:-`&not`(x[3])]

_m1897409280096, _m1897409281184

Exchanging x[1] with x[2], and (not x[1]) with (not x[2]) leads to a logically equivalent expression, so this is indeed a symmetry.

zip(`=`, L, L[convert(g1, permlist, nops(L))]); q1 := eval(q, %); Equivalent(q, q1)

[x[1] = x[2], x[2] = x[1], x[3] = x[3], Logic:-`&not`(x[1]) = Logic:-`&not`(x[2]), Logic:-`&not`(x[2]) = Logic:-`&not`(x[1]), Logic:-`&not`(x[3]) = Logic:-`&not`(x[3])]

Logic:-`&and`(Logic:-`&or`(x[2], x[1]), x[3])


Exchanging x[3] with (not x[3]) leads to an expression that perhaps has the same form but is not equivalent

zip(`=`, L, L[convert(g2, permlist, nops(L))]); q2 := eval(q, %); Equivalent(q, q2)

[x[1] = x[1], x[2] = x[2], x[3] = Logic:-`&not`(x[3]), Logic:-`&not`(x[1]) = Logic:-`&not`(x[1]), Logic:-`&not`(x[2]) = Logic:-`&not`(x[2]), Logic:-`&not`(x[3]) = x[3]]

Logic:-`&and`(Logic:-`&or`(x[1], x[2]), Logic:-`&not`(x[3]))




Please Wait...