1
Basic theory of magmas
▶
1.1
Alternate formula
2
Selected laws
▶
2.1
Equations of order greater than \(4\)
3
General implications
4
Implications between selected laws
5
Finite implications and infinite models
▶
5.1
Austin laws
5.2
Austin implications
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
Magma cohomology
12
Weak central groupoids
▶
12.1
Twisting a weak central groupoid
13
Equation 677
▶
13.1
A finite non-right-cancellative example
13.2
The free 677 magma
14
Equation 854
▶
14.1
Some further properties of 854 magmas
14.2
Running a greedy algorithm
14.3
The free 854 magma
15
Equation 906
16
Equation 1323
17
Equation 1516
18
Equation 1729
19
Rewriting theory
20
Order 5 Austin laws
▶
20.0.1
Equations with trivial finite models
20.0.2
Remaining unknown equations
21
Simple rewrites
22
Trivial auto-generated theorems
23
Enumerating Small Finite Magmas
24
Equation Search
25
E-Graphs
▶
25.1
lean-egg
25.2
MagmaEgg
26
Using the Vampire theorem prover
27
Bibliography
Dependency graph
Equational Theories
Contributors of the Equational Theories Project
1
Basic theory of magmas
1.1
Alternate formula
2
Selected laws
2.1
Equations of order greater than \(4\)
3
General implications
4
Implications between selected laws
5
Finite implications and infinite models
5.1
Austin laws
5.2
Austin implications
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
Magma cohomology
12
Weak central groupoids
12.1
Twisting a weak central groupoid
13
Equation 677
13.1
A finite non-right-cancellative example
13.2
The free 677 magma
14
Equation 854
14.1
Some further properties of 854 magmas
14.2
Running a greedy algorithm
14.3
The free 854 magma
15
Equation 906
16
Equation 1323
17
Equation 1516
18
Equation 1729
19
Rewriting theory
20
Order 5 Austin laws
20.0.1
Equations with trivial finite models
20.0.2
Remaining unknown equations
21
Simple rewrites
22
Trivial auto-generated theorems
23
Enumerating Small Finite Magmas
24
Equation Search
25
E-Graphs
25.1
lean-egg
25.2
MagmaEgg
26
Using the Vampire theorem prover
27
Bibliography