The purpose of this project is to explore the space of equational theories of magmas, ordered by implication. To begin with we shall focus only on theories of a single equation, which are listed here.
A (manually created) graph of the dependencies obtained so far can be found here, current as of Sep 26 2024.
Links:
- Main web page
- A blog post describing the project., Sep 25 2024.
- Initial discussion on Zulip, Sep 26 2024.
- Initial discusson on Mastodon, Jul 18 2023.
- Followup discussion on Mastodon, Sep 25 2024.
- The MathOverflow post that inspired the project, Jul 17 2023.
- A related MathOverflow post, Jul 16 2023.
- Automated provers for equational theories
- Prover9 and Mace4
- Vampire
- "Guided Equality Saturation", Thomas Kœhler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer, Jan 5 2024.
- "Rewrite Rule Inference Using Equality Saturation", Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, Zachary Tatlock, 23 Aug 2021.
- Other tools