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. various first-order languages and theories. As underlying theories there are real closed fields (real numbers with order), p-adic valued fields (p-adic numbers), and algebraically closed fields (complex numbers) available. This document describes the usage of REDLOG from the algebraic mode of REDUCE. REDLOG 2.0 is part of REDUCE 3.7.
Erika Cetindag, Martin Griebl