In this paper, we address algebraic issues of the quantifier elimination problem in Presburger arithmetic. First, we revisit, in a unified presentation, different techniques from polyhedral geometry that can support quantifier elimination over the integers. Second, we discuss optimizations for one of these techniques by taking advantages of parametric systems of multivariate linear congruences. Third, we report on a comparative implementation of these different strategies for quantifier elimination in Presburger arithmetic. Fourth, we apply these results and propose a new algorithm for performing parametric integer linear programming and report on its implementation. (c) 2026 Published by Elsevier Ltd.
Let K be an algebraic number field and R an order of K. The R-centralizer of T∈Mat(n,K) is the arithmetic group CR(T)×={Q∈GL(n,R)|QT=TQ}. We show that if CR(T)× is solvable-by-finite, then it is polycyclic and unipotent-by-abelian. We introduce a practical algorithm to compute generators for CR(T)× in this case. Our algorithm extends to compute the centralizer of a finite set of matrices or of subgroups in GL(n,R) in special cases.
In this paper we study the computational complexity of checking identities in involution monoids of order six or less. It is shown that the 6-element involution Brandt monoids (B21,∗1) and (B21,∗2) with two different involutions ∗1 and ∗2 are the exactly two smallest involution monoids for which the identity checking problems are coNP-complete, and all other involution monoids of order six or less for which this problem is decidable in polynomial time.
In (Hashemi and Kapur, 2025), we proposed an algorithm for converting a given Gröbner basis into a Gröbner basis with respect to another term ordering. A recent counterexample due to Heisel and Lauritzen (2025) shows that the presented algorithm is not correct as stated. In this short note, we identify the precise source of the failure, propose a corrected variant of the algorithm and prove that it returns, in finitely many steps, a Gröbner basis with respect to the target term ordering.
