Message Boards Message Boards


Unexpected behaviour from AxiomaticTheory["RingAxioms"]?

Posted 1 year ago
2 Replies
5 Total Likes

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.

2 Replies

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.

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract