Message Boards Message Boards

2
|
4265 Views
|
2 Replies
|
5 Total Likes
View groups...
Share
Share this post:

Unexpected behaviour from AxiomaticTheory["RingAxioms"]?

Posted 3 years ago

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.

POSTED BY: Bruce Colletti
2 Replies
Posted 3 years ago

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.

POSTED BY: Bruce Colletti

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!

POSTED BY: Mano Namuduri
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract