Constructive quantifier elimination with a focus on matrix rings. - Max Illmer; Tim Netzer (Ann. Pure Appl. Log., 2026)