On Computational Complexity of Semilinear Varieties
Enrico Marchioni · Journal of Logic and Computation · 2008
We propose a method for characterizing the complexity of satisfiability and tautologicity of equational theories of varieties of algebras by relying on their representability in the theory of the ordered additive group of reals R with rational constants. We call semilinear those varieties which are generated by a subclass of algebras in which the operations are representable as semilinear functions with rational coefficients. Those functions are definable in the theory of R which admits quantifier elimination and whose existential theory is NP-complete. We prove that there is a polynomial time translation of the equational theories of semilinear varieties into the existential theory of R. Then, if the variety is generated (up to isomorphism) by one semilinear algebra, the satisfiability problem is in NP, while the tautologicity problem is in co-NP. We apply this method in order to provide a comprehensive study of complexity of several varieties related to logics based on left-continuous conjunctive uninorms and left-continuous t-norms.