Two algorithms to decide Quantifier-free Definability in Finite Algebraic Structures

03/29/2023
by   Miguel Campercholi, et al.
0

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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset