1
Basic theory of magmas
2
Selected laws
▶
2.1
Equations of order greater than \(4\)
3
Infinite models
4
General implications
5
Implications between selected laws
6
Selected magmas
7
Infinite magma constructions
▶
7.1
Translation-invariant magmas
7.2
The Asterix equation
7.3
Obelix
7.4
Greedy algorithm constructions
7.5
A survey of examples
7.6
The Dupont equation
7.7
An ad hoc model
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
Weak central groupoids
▶
11.1
Twisting a weak central groupoid
12
Equation 854
▶
12.1
Some further properties of 854 magmas
12.2
Running a greedy algorithm
12.3
The free 854 magma
13
Equation 1323
14
Equation 1516
15
Rewriting theory
16
Simple rewrites
17
Trivial auto-generated theorems
18
Enumerating Small Finite Magmas
19
Equation Search
20
E-Graphs
▶
20.1
lean-egg
20.2
MagmaEgg
21
Using the Vampire theorem prover
22
Bibliography
Dependency graph
Equational Theories
Contributors of the Equational Theories Project
1
Basic theory of magmas
2
Selected laws
2.1
Equations of order greater than \(4\)
3
Infinite models
4
General implications
5
Implications between selected laws
6
Selected magmas
7
Infinite magma constructions
7.1
Translation-invariant magmas
7.2
The Asterix equation
7.3
Obelix
7.4
Greedy algorithm constructions
7.5
A survey of examples
7.6
The Dupont equation
7.7
An ad hoc model
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
Weak central groupoids
11.1
Twisting a weak central groupoid
12
Equation 854
12.1
Some further properties of 854 magmas
12.2
Running a greedy algorithm
12.3
The free 854 magma
13
Equation 1323
14
Equation 1516
15
Rewriting theory
16
Simple rewrites
17
Trivial auto-generated theorems
18
Enumerating Small Finite Magmas
19
Equation Search
20
E-Graphs
20.1
lean-egg
20.2
MagmaEgg
21
Using the Vampire theorem prover
22
Bibliography