The Redlog Home Page Redlog provides an extension of the computer algebra system Reduce to a computer logic system. The name stands for Reduce logic system. Redlog is an integral part of the open-source computer algebra system Reduce, which is available on Sourcefore. See the DOWNLOADS section for details. Redlog implements symbolic algorithms on first-order formulas with respect to user-chosen first-order languages and theories. The available domains include real numbers, integers, complex numbers, p-adic numbers, quantified propositional calculus, term algebras. Our group offers consulting and technical support for commercial applications of Redlog.