完全生成拟簇的可容许性
Admissibility in Finitely Generated Quasivarieties
摘要:
检查拟方程在一个随机生成(即,由有限代数的有限集合生成的)拟簇Q相当于在拟簇的适当的有限自由代数中检查有效性,因此是可判定的。然而,由于自由代数可能是大的,即使是小集合的小代数和非常少的生成元,这种天真的方法来检查在$\Q$的容许计算是不可行的。在本文中,算法的介绍,产生一个最小的(相对于一个多集良好的顺序在他们的基数)有限集的代数,使有效性的准方程在这个集合中对应的准方程在Q的容许性。特别是,结构完备性(有效性和容许性一致)和几乎结构完备性(有效性和容许性一致的准方程与统一的前提)可以检查。该算法说明了一个选择著名的生成的拟变种,并适应于处理有限值逻辑中的规则的可接受性。
英文摘要:
Checking the admissibility of quasiequations in a finitely generated (i.e., generated by a finite set of finite algebras) quasivariety Q amounts to checking validity in a suitable finite free algebra of the quasivariety, and is therefore decidable. However, since free algebras may be large even for small sets of small algebras and very few generators, this naive method for checking admissibility in $\Q$ is not computationally feasible. In this paper, algorithms are introduced that generate a minimal (with respect to a multiset well-ordering on their cardinalities) finite set of algebras such that the validity of a quasiequation in this set corresponds to admissibility of the quasiequation in Q. In particular, structural completeness (validity and admissibility coincide) and almost structural completeness (validity and admissibility coincide for quasiequations with unifiable premises) can be checked. The algorithms are illustrated with a selection of well-known finitely generated quasivarieties, and adapted to handle also admissibility of rules in finite-valued logics.
机构、总结、中文摘要均由AI分析而来,可能存在错误,请以论文正文为准。