In WL 12.2, AxiomaticTheory@“RingAxioms” returns 1-sided distributivity.
But 2-sided distributivity characterizes a ring.
Why does RingAxioms behave this way?
It seems that a new theory (say NearRingAxioms) could treat 1-sided distributivity so that RingAxioms could treat 2-sided distributivity. Nevertheless, there’s undoubtedly a good reason that RingAxioms uses 1-sided distributivity.
Hi Bruce!
We had expanded out ring axioms to four cases based on whether there is multiplicative identity and/or commutativity. One-sided distributivity is sufficient for commutative rings, but you are right that otherwise, we should be using two-sided distributivity. This will be fixed for the next release - thanks for catching this!
Thank you, Mano. We’re all watching how your team enhances theorem proving in WL, as more theories are added to AxiomaticTheory.
I may post other questions as this 6-session course on Theorem Proving progresses. John McGee teaches it thru Tech Services, and each session is the week’s highlight.