16.53 REDLOG: Extend REDUCE to a computer logic system

The name REDLOG stand for REDuce LOGic system. 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.

Documentation for this package can be found online.

Authors: Andreas Dolzmann and Thomas Sturm