This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We show the problem to be coNP-complete and present two decision algorithms based on a semantical characterization of definable relations as those preserved by isomorphisms of substructures, the second one also providing a formula in the positive case. Our approach also includes the design of an algorithm that computes the isomorphism type of a tuple in a finite algebraic structure. Proofs of soundness and completeness of the algorithms are presented, as well as empirical tests assessing their performances.

翻译：本文研究有限代数结构上无量子一阶公式的定义性问题。我们证明了该问题是coNP完全的，并基于可定义关系在子结构同构下保持不变的语义刻画，提出了两种判定算法；其中第二种算法在肯定情况下还能给出具体公式。我们的方法还包括设计一种算法，用于计算有限代数结构中元组的同构类型。文中给出了算法的可靠性与完备性证明，并通过实证测试评估了其性能表现。