发表机构
CNRS; Sorbonne Université（法国国家科学研究中心; 索邦大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究了结合二元运算阶数至多4的653个等式定律的合取，确定了456个等价类及其蕴含关系，构成半格，并在Lean中形式化，是等式理论项目的半群类比。
AI 中文摘要
我们考虑结合二元运算的阶数至多4的653个等式定律及其所有合取。我们确定这样的合取（结合等式理论）仅有456个等价类，并找出它们之间的所有蕴含关系。合取运算使这一理论集合构成一个半格。这些结果已在Lean中形式化。这是等式理论项目的半群类比，但扩展到了方程的合取。
英文摘要
We consider the 653 equational laws of order up to 4 for an associative binary operation, and all of their conjunctions. We determine that there are only 456 equivalence classes of such conjunctions (associative equational theories), and find all implications between them. The conjunction operation makes this set of theories into a semi-lattice. These results are formalized in Lean. This is a semigroup analogue of the Equational Theories Project, but extended to conjunctions of equations.
Comments13 pages plus long appendices with lists of equations
