有限代数的公理化

我们证明了在有限代数类 $\mathcal{A}$ 中有效的 $n$ 元公式集始终是一种正则树语言，并计算出了 $\mathcal{A}$ 的有限公理集。我们对 Barzdins 液流算法 (Barzdin+Barzdin, 1991) 进行了理性重构。我们展示了对于给定理论 $T$，存在原型代数类 $\mathcal{A}$ 的充分条件。这样的集合使我们能够通过测试 $p$ 是否在 $\mathcal{A}$ 中成立来证明 $T \models p$。