We automatically check for the feasibility of arbitrary boolean combinations of linear parametric p-adic constraints using a quantifier elimination method. This can be done uniformly for all p. We focus on the necessary simplification methods. Our method is implemented within the computer algebra system REDUCE. We illustrate the applicability of this implementation to non-trivial problems including the solution of systems of linear congruences over the integers.
Erika Cetindag, Martin Griebl