REDLOG stands for REDUCE LOGIC system. It provides an extension of the computer algebra system REDUCE to a "computer logic system" implementing symbolic algorithms on first-order formulas wrt. temporarily fixed first-order languages and theories. Underlying theories currently available are ordered fields and discretevly valued fields. Though the focus of the implemented algorithms is on effective quantifier elimination and simplification of quantifier-free formulas, REDLOG is intended and designed as an all-purpose system. REDLOG is freely available to the scientific community.
Ulrike Peiker, Martin Griebl