We study computational aspects of first-order logic and its extensions in the semiring semantics developed by Gr\"adel and Tannen. We characterize the complexity of model checking and data complexity of first-order logic both in terms of a generalization of BSS-machines and arithmetic circuits defined over $K$. In particular, we give a logical characterization of $\mathrm{FAC}^0_{K}$ by an extension of first-order logic that holds for any $K$ that is both commutative and positive.

翻译：我们在Gr\"adel和Tannen提出的半环语义框架下，研究一阶逻辑及其扩展的计算特性。通过定义在$K$上的广义BSS机模型和算术电路，我们刻画了一阶逻辑模型检验的复杂度及其数据复杂度。特别地，对于任意满足交换性与正性的$K$，我们通过一阶逻辑的扩展形式给出了$\mathrm{FAC}^0_{K}$的逻辑特征刻画。