Two algorithms to decide Quantifier-free Definability in Finite Algebraic Structures
Logic in Computer Science
2023-03-31 v1 Logic
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.
Cite
@article{arxiv.2303.17017,
title = {Two algorithms to decide Quantifier-free Definability in Finite Algebraic Structures},
author = {Miguel Campercholi and Mauricio Tellechea and Pablo Ventura},
journal= {arXiv preprint arXiv:2303.17017},
year = {2023}
}