Deciding Quantifier-free Definability in Finite Algebraic Structures

CAMPERCHOLI, MIGUEL; TELLECHEA, MAURICIO; VENTURA, PABLO

THEORETICAL COMPUTER SCIENCE

ELSEVIER SCIENCE BV

Lugar: Amsterdam; Año: 2020 vol. 348 p. 23 - 41

0304-3975

This work deals with the definability problem by quantifier-free first-order formulas over a finite algebraic structure. We showthe problem to be coNP-complete and present a decision algorithm based on a semantical characterization of definable relationsas those preserved by isomorphisms of substructures. Our approach also includes the design of an algorithm that computes theisomorphism 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.