Authors: Andreas Dolzmann and Thomas Sturm
REDLOG provides an extension of the computer algebra system REDUCE to a computer logic system. The name stands 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, combination of reals with integers, complex numbers, p-adic numbers, quantified propositional calculus, term algebras, queues.
Redlog originated from the implementation of real quantifier elimination.
- www.redlog.eu - the REDLOG homepage