Two algorithms to decide Quantifier-free Definability in Finite Algebraic Structures
From MaRDI portal
Publication:6431344
DOI10.1016/J.ENTCS.2020.02.003arXiv2303.17017WikidataQ113317344 ScholiaQ113317344MaRDI QIDQ6431344FDOQ6431344
Authors: Miguel Campercholi, Mauricio Tellechea, Pablo Ventura
Publication date: 29 March 2023
Abstract: 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.
Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Decidability of theories and sets of sentences (03B25) Logic in computer science (03B70)
This page was built for publication: Two algorithms to decide Quantifier-free Definability in Finite Algebraic Structures
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6431344)