Equational theories
1
Basic theory of magmas
2
Selected laws
3
Infinite models
4
General implications
5
Implications between selected laws
6
Selected magmas
7
The Asterix equation
8
Equivalence with the constant and singleton laws
9
Metatheorems from Invariants
▶
9.1
Invariants
9.2
Expanding the language
9.3
Proving metatheorems from invariants in Lean
9.4
Generating laws from equations
9.5
Conclusion: Beyond Invariants
10
Some abstract nonsense
▶
10.1
Confluent theories
11
Simple rewrites
12
Trivial auto-generated theorems
13
Enumerating Small Finite Magmas
14
Equation Search
15
E-Graphs
▶
15.1
lean-egg
15.2
MagmaEgg
16
Using the Vampire theorem prover
17
Bibliography
Dependency graph
13 Enumerating Small Finite Magmas
describe the process of automatically generating these implications here.