Decidability of elementary theories of certain finitely defined algebras (Q1803020)

The paper introduces some conditions ensuring that a finitely defined algebra \(G\) (with generators \(A\) and defining relations \(S\)) in a variety defined by the finite set of identities \(\Sigma\) have a decidable first order theory. The conditions essentially involve the rewriting relation on terms (freely generated from \(A\)) induced by \(S\) and \(\Sigma\); in one case it is assumed to be Noetherian; in the second case this assumption is dropped --- and other conditions are required.